Coq is an interactive theorem prover and functional programming language based on the calculus of inductive constructions, developed beginning in 1984 at INRIA in France by a team including Thierry Coquand and Gerard Huet. Coq allows a user to write mathematical definitions, state formal theorems, and construct machine-checked proofs of those theorems, with programs and their correctness proofs expressed within the same dependently typed functional language; Coq has been used to formally verify substantial pieces of software and mathematics, including the CompCert verified C compiler and a machine-checked proof of the four color theorem.
Facts
First Released SignificanceUsed to program and prove correct the CompCert optimizing C compiler. 2 Connections
Associated With
Sibling interactive proof assistants.
In Field
Licensed Under
Entity-backed identity for the license enum value this item already carries, resolved to a software license concept by an explicit value-to-entity map (phase 3 bucket conversion, docs\design_entity_backed_browse_buckets_20260928.md). The license fact itself stays on the item unchanged.
Sources
1. Wikidata: Rocq prover
- Wikidata Q1131652, resolved via en.wikipedia pageprops (wave rule R-L)
- Wikidata Q1131652 P275 (license)
- Wikidata P577 (publication/release date)
View the Source2. Rocq - Wikipedia
Notable uses, Other applications
CompCert: an optimizing compiler for almost all of the C programming language which is largely programmed and proven correct in Rocq.
- In Field: Formal Methods, Lead paragraph
View the SourceDependent type (Wikipedia)
In Group: Dependently Typed Proof Assistant Languages, article names Rocq (Coq) among functional languages using dependent types to help reduce bugsView the Source Reader Challenges (0)
No disputes yet. Spotted an error or a better source? Open the first one.
Sign in to dispute this or suggest a correction.