Lean theorem prover/History/The Calculus of Constructions

Lean theorem prover: map
Reading the edition Three levels of reading Glossary Notation Chronology
Reading by level Start here: What a proof assistant does The type theory: Terms, types and judgments How Lean works: Elaboration The history: Automath The applications: Research mathematics
Sources Sources Bibliography Further reading
Related The move to Lean

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.

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.

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.

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. Lean's Prop has the same property; see 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. Version 4.4 of the software, frozen in March 1988, already offered inductive types encoded in this way.

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. The result is the Calculus of Inductive Constructions. Its rules were set out by Paulin-Mohring in 1993. In Lean every inductive type comes with a recursor that is its induction principle; see 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. The name referred to the Calculus of Constructions, to Thierry Coquand, and to the rooster, a French national symbol.

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. 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. The idea is followed at LCF and the tactic idea.

In 2013 the ACM Software System Award was given to the team that first developed Coq. 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. The new name honours Inria Rocquencourt, where the prover was first developed.

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.

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. 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. These features of Lean are treated at Proof irrelevance and subsingleton elimination, Quotient types and Structural and well-founded recursion.

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.

Next

Lean 1 to Lean 3