&sq=&lang=&file=File:Coq_logo.png){kind=logo} | |
| Developer(s) | The Coq development team |
|---|---|
| Initial release | 1 May 1989 (version 4.10) |
| Stable release | 8.20.0[1] 
/ 3 September 2024 |
| Repository | github |
| Written in | OCaml |
| Operating system | Cross-platform |
| Available in | English |
| Type | Proof assistant |
| License | LGPLv2.1 |
| Website | coq |
&sq=&lang=&file=File:Coq_8.5_stdlib_proof.png)
Coq is an interactive theorem prover first released in 1989. It allows for expressing mathematical assertions, mechanically checks proofs of these assertions, helps 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 (procedures) and various decision procedures.
The Association for Computing Machinery awarded Thierry Coquand, Gérard 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.
The name "Coq" is a wordplay on the name of Thierry Coquand, Calculus of Constructions or "CoC" and follows the French computer science tradition of naming software after animals (coq in French meaning rooster).[2] On October 11th, 2023, the development team announced that Coq will be renamed "The Rocq Prover" in the coming months, and has started updating the code base, website and associated tools.[3]
- ^ "Release Coq 8.20.0". 3 September 2024.
- ^ "Alternative names · coq/coq Wiki". GitHub. Retrieved 3 March 2023.
- ^ "Coq roadmap 069". GitHub.