Primary evidence
- Coq / Rocq historical notesS2 · Official institutional · Official announcement
The Calculus of Constructions proof checker begins the Coq lineage
The system provided machine checking for proofs in the Calculus of Constructions and evolved through successive implementations into Coq and later Rocq.
What happened?
The official Coq/Rocq history records version 1.10 as frozen on 22 December 1984, during the initial implementation of a Calculus of Constructions proof checker by Thierry Coquand and Gérard Huet.
Why it matters
Coq later supported major formalized-mathematics achievements and became an important environment for machine-learning and AI-assisted theorem proving.
Significance rationale: The early Calculus of Constructions checker became the direct lineage of Coq, establishing dependent-type proof checking as a durable platform for formal mathematics and mechanized reasoning.
Historical context
Earlier developments
—
Later developments
—
Related milestones
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Claimed
- Evidence level
- E2 · Research record
- AI role
- Computation only
- Formal assurance
- No formal assurance
Contribution & verification
- Mathematical novelty
- Tooling only
- Interface
- Formal, Symbolic
- AI contribution
- The system mechanically checked formal proof terms; humans supplied the formal statements and proof constructions.
- Human contribution
- Thierry Coquand, Gérard Huet and collaborators designed the type theory and implemented the early checker.
- Verification
- Claimed · E2 · Research record · No formal assurance
- Last reviewed
- 2026-09-15
Technical details
- Systems
- coq, calculus-of-constructions
- Organizations
- inria
- Problems
- formal-proof-checking
- Methods
- dependent-type-theory, proof-checking, calculus-of-constructions
Sources & artifacts
- Coq / Rocq historical notesS2 · Official institutional · Official announcement · accessed 2026-09-15
Verification history
- 1984-12-22 · Claimed · E2 · Research record
The official project history supplies the dated version record and describes the initial Calculus of Constructions implementation.
Corrections
No corrections recorded.