Calculus of Constructions

The Calculus of Constructions (CC) is a type theory that combines features of Martin-Löf type theory with higher-order polymorphism, aka System F_\omega.

It was introduced by Thierry Coquand in his 1985 PhD thesis, and later published in the journal article Coquand and Huet 1988.

Description

From Martin-Löf's type theory, CC has adopted contexts, dependent products, and a universe \textsf{Prop} of propositions.

From System F_\omega, CC has adopted impredicative quantification over the universe \textsf{Prop} of propositions.
That is to say that the product of a family x : A \vdash P : \textsf{Prop} of propositions is again a proposition \vdash \forall x : A.\ P : \textsf{Prop}. Thus, a part of this system is impredicative.

Encoding data types in CC

CC contains no other primitives. As such, all types must be encoded through impredicative quantification, as in System F_\omega.

For example, writing A : \textsf{Prop} \vdash \textsf{Prf}(A)\ \textsf{type} for the decoding map of the universe, we can encode the natural numbers by

  \textsf{Nat} = \textsf{Prf}(
    \forall c : \textsf{Prop}.\ \forall z : \textsf{Prf}(c).
      \ \forall s : \textsf{Prf}(c) \to \textsf{Prf}(c).\ c
  )

However, this runs into the usual problem: the defined data types do not have elimination rules/induction principles.

There are two solutions to this:

switch to the Extended Calculus of Constructions
switch to the Calculus of Inductive Constructions

References

CC was introduced in

Coquand, Thierry. 1985. ‘Une Théorie Des Constructions’. PhD thesis, University of Paris VII.

@phdthesis{coquand_theorie_1985,
	type = {{PhD} thesis},
	title = {Une {Théorie} des {Constructions}},
	school = {University of Paris VII},
	author = {Coquand, Thierry},
	year = {1985},
}

Coquand, Thierry, and Gérard Huet. 1988. ‘The Calculus of Constructions’. Information and Computation 76 (2–3): 95–120. https://doi.org/10.1016/0890-5401(88)90005-3.

@article{coquand_calculus_1988,
	title = {The calculus of constructions},
	volume = {76},
	issn = {10902651},
	doi = {10.1016/0890-5401(88)90005-3},
	number = {2-3},
	journal = {Information and Computation},
	author = {Coquand, Thierry and Huet, Gérard},
	year = {1988},
	pages = {95--120}
}

Much of the information on this page comes from section 2.2.3 of

Hofmann, Martin. 1997. ‘Syntax and Semantics of Dependent Types’. In Semantics and Logics of Computation, edited by Andrew M. Pitts and P. Dybjer, 79–130. Cambridge University Press. https://doi.org/10.1017/CBO9780511526619.004. pdf

@incollection{hofmann_1997,
	title = {Syntax and {Semantics} of {Dependent} {Types}},
	url = {https://www.tcs.ifi.lmu.de/mitarbeiter/martin-hofmann/pdfs/syntaxandsemanticsof-dependenttypes.pdf},
	booktitle = {Semantics and {Logics} of {Computation}},
	publisher = {Cambridge University Press},
	author = {Hofmann, Martin},
	editor = {Pitts, Andrew M. and Dybjer, P.},
	year = {1997},
	doi = {10.1017/CBO9780511526619.004},
	pages = {79--130}
}