Our website is made possible by displaying online advertisements to our visitors.
Please consider supporting us by disabling your ad blocker.
Coq (software)
&sq=crain_ford&lang=en&file=File:Coq_logo.png){kind=logo} | |
| Original author(s) | Thierry Coquand, Gérard Huet, Christine Paulin-Mohring, Bruno Barras, Jean-Christophe Filliâtre, Hugo Herbelin, Chetan Murthy, Yves Bertot, Pierre Castéran |
|---|---|
| Developer(s) | INRIA, École Polytechnique, University of Paris-Sud, Paris Diderot University, CNRS, ENS Lyon |
| 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=crain_ford&lang=en&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 11, 2023, the development team announced that Coq will be renamed The Rocq Prover in coming months, and began 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.
Previous Page Next Page
