The calculus of constructions

In May 1986 Thierry Coquand and Gérard Huet of INRIA issued a report on the calculus of constructions, a higher-order formalism in which every proof is a lambda expression typed with the proposition it proves. Remove the types and what remains is the program corresponding to the proof. The authors proved strong normalisation: every computation terminates, so the logic is consistent.

The report rests on the Curry-Howard correspondence between propositions and types and says that for computer science it yields a very high-level functional language in which a type can be an arbitrarily complex specification of a program. The terms, the authors say, are inspired by the Automath formalisms, with de Bruijn's indexes. The report has no measurement: it is a theory, not a system. The link to Lean rests on its authors' 2015 paper: Lean's kernel can provide a version of the calculus of inductive constructions, citing Coquand and Huet. What the record does not claim: when the first version of Coq was released; the documents read do not say.