CoQ

Coq (software)

Developer(s)	The Coq development team
Initial release	May 1, 1989; 27 years ago (1989-05-01) (version 4.10)
Stable release	8.6 / December 14, 2016 (2016-12-14)
Repository	scm.gforge.inria.fr/anonscm/git/coq/coq.git/
Development status	Active
Written in	OCaml
Operating system	Cross-platform
Available in	English
Type	Proof assistant
License	LGPL 2.1
Website	coq.inria.fr

In computer science, Coq is an interactive theorem prover. It allows the expression of mathematical assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification. Coq works within the theory of the calculus of inductive constructions, a derivative of the calculus of constructions. Coq is not an automated theorem prover but includes automatic theorem proving tactics and various decision procedures.

The Association for Computing Machinery presented Coquand, Huet, Paulin-Mohring, Barras, Filliâtre, Herbelin, Murthy, Bertot, Castéran with the 2013 ACM Software System Award for Coq.

Seen as a programming language, Coq implements a dependently typed functional programming language, while seen as a logical system, it implements a higher-order type theory. The development of Coq has been supported since 1984 by INRIA, now in collaboration with École Polytechnique, University of Paris-Sud, Paris Diderot University and CNRS. In the 1990s, École Normale Supérieure de Lyon was also part of the project. The development of Coq was initiated by Gérard Huet and Thierry Coquand, after which more than 40 people, mainly researchers, contributed features of the core system. The implementation team was successively coordinated by Gérard Huet, Christine Paulin and Hugo Herbelin. Coq is for the most part implemented in OCaml with a bit of C. The core system can be extended thanks to a mechanism of plug-ins.