Coq proof assistant

Coq (programming language)
Dialects
Paradigm	Functional
First appeared	1984
Typing discipline	static, strong
Filename extensions	.v
Website	coq.inria.fr
LEGO (proof assistant)
Influenced by
ML (programming), LCF (proof methods), Automath (hybrid programming/proving), System F and intuitionistic type theory (language)
Influenced
Agda, Idris, Matita, Albatross

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 rewarded Thierry Coquand, Gérard Pierre Huet, Christine Paulin-Mohring, Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin, Chetan Murthy, Yves Bertot and Pierre 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 Pierre 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 Pierre Huet, Christine Paulin-Mohring 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.