Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the formalization of programming languages semantics (e.g. the CompCert compiler certification project or Java Card EAL7 certification in industrial context), the formalization of mathematics (e.g. the full formalization of the 4 color theorem or constructive mathematics at Nijmegen) and teaching.

1970 年代：Gérard Huet 开始在自动定理证明方面进行工作，使用LISP 语言实现了带等式的一阶逻辑证明器SAM。λ 演算成为研究证明论的主要工具。Jean-Yves Girard 证明了分析的一致性，他的证明使用了称为System-F 的多态λ 演算中证明的终止性。这一系统被推广到一个表示多态泛函的Fω 系统，因而可为一类超出了传统序数层次的算法进行编码。John Reynolds 在推广ML 语言的受限制的多态结构时，又重新实现了这一系统。

1980年代：Knuth 和Bendix 开展了奠基性研究工作。Jean-Marie Hullot 和Gérard Huet完成了一个KB 软件，它以一种自然的方式实现代数结构的自动判定过程和半可判定过程。同时，归纳证明领域也取得了稳步的进展，最著名的工作是Boyer 和Moore 的NQTHM/ACL 系统。同时，逻辑学家（Dana Scott ）和理论计算机科学家（Gordon Plotkin 、Gilles Kahn、Gérard Berry ）正在研究可计算函数的一种逻辑理论（可计算论域），以及有效可用公理化（可计算归纳），目的是为了定义程序语言的语义。Gérard Huet 联合巴黎高等师范学院的Guy Cousineau 和Pierre-Louis Curien 在INRIA Rocquencourt 实验室启动了Formel 项目。他们准备把ML 语言不仅用于定义tactics，同时用于实现整个系统。这一项在函数式方面的研究和开发工作在几年后产生了CAML 语言族，最终导致了今天的Objective Caml 语言，它就是现在的Coq 证明器的实现语言。1984 年，Gilles Kahn 在Sophia Antipolis 组织了一个类型理论的国际会议，在会上，Thierry Coquand 和Gérard Huet 展示了一个把依赖类型和多态类型综合在一起的系统，它把MartinL.f 的构造性理论融入了Automath 系统的一个扩展，该系统命名为构造演算（Calculus of Constructions）。1989 年，Coq 4.1 版本发布，该版首次加入了由Benjamin Werner 所设计的从证明中抽取函数式程序（Caml 语法）的机制。

1990 年代：推出的Coq 5.6 版提供了进行数学描述的统一语言（Gallina“vernacular”），原始归纳类型，从证明中抽取程序的机制，和一个图形化用户界面。1996 年11 月发布的Coq 6.1 版引入了所有上述理论成就，也包括了几项对提高效率有关键作用的技术，特别是Bruno Barras 的规约机制，

2000年以后：Coq 系统经历了完全的重新设计，版本7拥有一个函数式核心，主要架构师是Jean-Christophe Filli.tre，Hugo Herbelin 和Bruno Barras 。一个用于tactics 设计的新语言由David Delahaye 开发出来，此后人们可以用高级语言为复杂的证明策略编程。为了对数值软件进行正确性验证，Micaela Mayero 研究了实数的公理化问题。同时，Yves Bertot 重新利用CtCoq 的思想，用Java 语言开发了一个复杂的图形界面PCoq 。2002 年Jacek Chr.aszcz 采用了类似Caml 的方法把模块和函子系统整合在一起。2003 年底，在经过对主要的输入语言进行重新设计之后发布了8.0 版本（目前版本8.4）。目前在应用方面，Coq 已经足够强壮，并可用作实现特定证明工具的低层语言

Coq迄今最为成功的应用在软件形式化验证方面。Trusted Logic 利用Coq成功地完成JavaCard 语言的整个执行环境的形式化验证。这项安全方面的工作获得EAL7 证书奖（公共标准下最高级别的奖励）。开发使用了121000 行Coq 代码，总共278 个模块。2013 年Coq获得ACM SIGPLAN编程语言软件奖。此外，Coq在数学定理辅助证明方面也有不少斩获，如“四色定理”证明（这样是否意味了数学和计算机变成真正的一家亲，天才的数学家们是否担心害怕自己的饭碗问题呢？随着计算机能力的快速增长， 再过二三十年， 大多数研究都将可以由计算机来做。 它们不仅能证明数学定理， 甚至可以发现数学定理，但就目前两个学科的发展现状而言，计算机至多只能起辅助作用，还不能代替人创造性的思考）。

值得关注的是，另一种基于高阶逻辑的定理辅助证明系统Isabelle也在研究和发展中，它进行函数式程序建模，多数证明只要两步完成：对所选变量进行归纳以及使用自动策略，能够处理集合、函数、关系以及实现递归定义集合，利用了嵌套递归和交叉递归等技术、大量可供选择使用的低级证明策略。

参考文献：

Coq官方网址：http://coq.inria.fr

Coq维基百科http://zh.wikipedia.org/wiki/Coq

 (德)Yves Bertot   Pierre Casteran 著，顾明 译。交互式定理证明与程序开发--Coq归纳构造演算的艺术。清华大学出版社，2010年