PMA Publisher: Published from the Principia Machina source

2026-10-15T19:35:28Z

Published from the Principia Machina source

← Older revision		Revision as of 19:35, 15 October 2026
Line 1:		Line 1:
	{{DISPLAYTITLE:The Calculus of Constructions}}		{{DISPLAYTITLE:The Calculus of Constructions}}
			{{Lean theorem prover map}}
	The Calculus of Constructions is a type theory introduced by Thierry Coquand and Gérard Huet in the mid-1980s. With inductive types added in 1989, it became the Calculus of Inductive Constructions, the logic of the proof assistant Coq, now called the Rocq Prover. Lean's logic is a member of the same family. This page follows the calculus from Coquand's thesis to the present and states where Lean departs from its relatives.		The Calculus of Constructions is a type theory introduced by Thierry Coquand and Gérard Huet in the mid-1980s. With inductive types added in 1989, it became the Calculus of Inductive Constructions, the logic of the proof assistant Coq, now called the Rocq Prover. Lean's logic is a member of the same family. This page follows the calculus from Coquand's thesis to the present and states where Lean departs from its relatives.

PMA Publisher: Published from the Principia Machina source

2026-10-14T18:01:13Z

Published from the Principia Machina source

New page

{{DISPLAYTITLE:The Calculus of Constructions}}
The Calculus of Constructions is a type theory introduced by Thierry Coquand and Gérard Huet in the mid-1980s. With inductive types added in 1989, it became the Calculus of Inductive Constructions, the logic of the proof assistant Coq, now called the Rocq Prover. Lean's logic is a member of the same family. This page follows the calculus from Coquand's thesis to the present and states where Lean departs from its relatives.

== Coquand's thesis and the first engine ==

Coquand and Huet both worked at INRIA. Coquand's thesis, which presented what was first called the Theory of Constructions, was defended on 31 January 1985. The Coq reference manual's history, written by Huet, Coquand and Christine Paulin-Mohring, describes the first software as a prototype type checker for that formalism, developed from late 1983 to early 1985 and mostly Huet's work. It names Girard's polymorphic System F and de Bruijn's Automath as influences; Huet's earlier summary in the same manual describes the calculus as combining Martin-Löf's type theory and Girard's polymorphic calculus in a higher-order extension of the Automath language. The prototype used a single binding operator for both the dependent product and function abstraction, in the manner of Automath, and handled substitution with de Bruijn indices.<ref name="rocqhist">The Rocq Prover Reference Manual, "History of Coq", including "A short history of the early versions" written by Thierry Coquand, Gérard Huet and Christine Paulin-Mohring in September 2015 and Huet's summary of February 1995. https://rocq-prover.org/doc/master/refman/history.html</ref>

A preliminary version of their paper on the calculus was presented at the International Symposium on Semantics of Data Types at Sophia-Antipolis in June 1984. Coquand and Huet described it at EUROCAL in 1985, and under its present name in an INRIA report of May 1986 and in the journal ''Information and Computation'' in 1988.<ref name="ch1986">Thierry Coquand and Gérard Huet, "The calculus of constructions", INRIA Research Report RR-0530, May 1986. https://inria.hal.science/inria-00076024</ref><ref name="ch1985">Thierry Coquand and Gérard Huet, "Constructions: a higher order proof system for mechanizing mathematics", in ''EUROCAL '85'', Lecture Notes in Computer Science 203, Springer, 1985, pp. 151–184. doi:10.1007/3-540-15983-5_13</ref><ref name="ch1988">Thierry Coquand and Gérard Huet, "The calculus of constructions", ''Information and Computation'' 76 (2–3), 1988, pp. 95–120. doi:10.1016/0890-5401(88)90005-3</ref>

== What the calculus says ==

In the 1986 report every proof is a lambda-expression whose type is the proposition it proves. Erasing the types leaves a pure lambda-term, the algorithm the proof contains, and computing with it corresponds to cut elimination. The authors call the correspondence between propositions and types, as Martin-Löf had advocated, a powerful paradigm for computer science. They prove that every computation in the calculus terminates, and obtain the consistency of the logic as a corollary. They also say that their terms are inspired by the Automath languages.<ref name="ch1986" />

The calculus is '''impredicative''': a proposition may be formed by quantifying over all propositions, itself included. Christine Paulin-Mohring's later introduction gives the standard example. The type of the polymorphic identity on propositions, "for every proposition ''X'', ''X'' implies ''X''", is itself a proposition. She adds that impredicativity is powerful but fragile. Only the sort of propositions may have it; making the next universe impredicative as well gives an inconsistent system.<ref name="pm2015">Christine Paulin-Mohring, "Introduction to the Calculus of Inductive Constructions", in B. Woltzenlogel Paleo and D. Delahaye (eds.), ''All about Proofs, Proofs for All'', Studies in Logic 55, College Publications, 2015. https://inria.hal.science/hal-01094195</ref> Lean's <code>Prop</code> has the same property; see [[Lean theorem prover/Foundations/Universes and Prop|Universes and Prop]].

== Inductive types ==

The pure calculus can encode natural numbers, lists and other data by impredicative definitions, but Paulin-Mohring records two drawbacks: functions over the encoded types compute inefficiently, and some natural properties of them cannot be proved.<ref name="pm2015" /> Version 4.4 of the software, frozen in March 1988, already offered inductive types encoded in this way.<ref name="rocqhist" />

Coquand and Paulin-Mohring then added inductive definitions as primitives, following the pattern of Martin-Löf's type theory. Their paper "Inductively defined types" was presented at COLOG-88 and published in 1990; the manual dates the extension to 1989.<ref name="rocqhist" /><ref name="cp1990">Thierry Coquand and Christine Paulin, "Inductively defined types", in P. Martin-Löf and G. Mints (eds.), ''COLOG-88'', Lecture Notes in Computer Science 417, Springer, 1990, pp. 50–66. doi:10.1007/3-540-52335-9_47</ref> The result is the '''Calculus of Inductive Constructions'''. Its rules were set out by Paulin-Mohring in 1993.<ref name="pm1993">Christine Paulin-Mohring, "Inductive definitions in the system Coq: rules and properties", in ''Typed Lambda Calculi and Applications (TLCA '93)'', Lecture Notes in Computer Science 664, Springer, 1993, pp. 328–345. doi:10.1007/BFb0037116</ref> In Lean every inductive type comes with a recursor that is its induction principle; see [[Lean theorem prover/Foundations/Inductive types and recursors|Inductive types and recursors]].

== Coq ==

At the end of 1989 the system was renamed Coq, for the Calculus of Inductive Constructions, with version 5.1.<ref name="rocqhist" /> The name referred to the Calculus of Constructions, to Thierry Coquand, and to the rooster, a French national symbol.<ref name="rocqabout">The Rocq Prover, "About" page, sections "An Overview of the Name's Evolution" and "Awards". https://rocq-prover.org/about</ref>

The early system already had the division of labour Lean has today. Its theorem prover ran tactics written in CAML "in the LCF fashion", and users could add their own.<ref name="rocqhist" /> From version 4.7 in 1988 the proof checker, called the Constructive Engine, was kept apart as the trusted core: a proof term assembled by tactics was checked again in full by the engine, so the tactics did not themselves need to be certified.<ref name="rocqhist" /> The idea is followed at [[Lean theorem prover/History/LCF and the tactic idea|LCF and the tactic idea]].

In 2013 the ACM Software System Award was given to the team that first developed Coq.<ref name="rocqabout" /> The project later took a new name. Version 9.0 of the Rocq Prover, issued on 12 March 2025, completed the renaming from the Coq Proof Assistant.<ref name="rocq9">The Rocq Prover, "Rocq 9.0.0" (announcement of version 9.0.0, 12 March 2025). https://rocq-prover.org/releases/9.0.0</ref> The new name honours Inria Rocquencourt, where the prover was first developed.<ref name="rocqabout" />

== Lean's place in the family ==

Lean implements a version of the Calculus of Inductive Constructions. Its developers have said so from the start: the 2015 system description presents Lean's trusted kernel as a version of it when the sort of propositions is impredicative, and the 2017 paper on Lean 3's metaprogramming cites Coquand and Huet (1988) and Coquand and Paulin (1990) for the logic.<ref name="lean2015">Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn and Jakob von Raumer, "The Lean Theorem Prover (system description)", in ''Automated Deduction – CADE-25'', Lecture Notes in Computer Science 9195, Springer, 2015, pp. 378–388. doi:10.1007/978-3-319-21401-6_26. Author's copy: https://lean-lang.org/papers/system.pdf</ref><ref name="ebner2017">Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad and Leonardo de Moura, "A metaprogramming framework for formal verification", ''Proceedings of the ACM on Programming Languages'' 1 (ICFP), article 34, 2017. doi:10.1145/3110278. Author's copy: https://lean-lang.org/papers/tactic.pdf</ref>

It is not the same theory as Coq's. Mario Carneiro's 2019 account of Lean's type theory lists the differences as they then stood. Coq's universes are cumulative, so that a type in one universe also belongs to every larger one, and Lean's are not. Coq's core language has primitive constructs for recursion and pattern matching, while Lean's kernel has only the recursors, and recursive definitions are compiled into them. Lean's definitions are polymorphic in universe levels. Lean has definitional proof irrelevance, any two proofs of a proposition being equal by definition, where Coq then had it only as an axiom. And Lean has quotient types with a computation rule.<ref name="carneiro2019">Mario Carneiro, ''The Type Theory of Lean'', thesis, April 2019, section 2.8 "Differences from Coq". https://github.com/digama0/lean-type-theory/releases/download/v1.0/main.pdf</ref> The 2015 description had already noted that, unlike Coq, Lean keeps fixed-point expressions, match expressions and the termination checker out of the Lean kernel.<ref name="lean2015" /> These features of Lean are treated at [[Lean theorem prover/Foundations/Proof irrelevance and subsingleton elimination|Proof irrelevance and subsingleton elimination]], [[Lean theorem prover/Foundations/Quotient types|Quotient types]] and [[Lean theorem prover/Foundations/Structural and well-founded recursion|Structural and well-founded recursion]].

<blockquote>
Provenance: the Rocq reference manual's history, the 1986 INRIA report, Paulin-Mohring's 2015 introduction, Carneiro's thesis, the two Lean papers and the Rocq project's pages were read. Coquand's thesis, the 1985, 1988, 1990 and 1993 papers were not opened; their details come from the publishers' records and the manual. The date of the decision to rename Coq was not verified and is not given.
</blockquote>

== Next ==

[[Lean theorem prover/History/Lean 1 to Lean 3|Lean 1 to Lean 3]]

== References ==
<references />

Lean theorem prover/History/The Calculus of Constructions - Revision history

PMA Publisher: Published from the Principia Machina source

PMA Publisher: Published from the Principia Machina source