The Calculus of Constructions (CC) is a type theory that combines features of Martin-Löf type theory with higher-order polymorphism, aka System .
It was introduced by Thierry Coquand in his 1985 PhD thesis, and later published in the journal article [Coquand and Huet 1988].
From Martin-Löf's type theory, CC has adopted contexts, dependent products, and a universe of propositions.
From System , CC has adopted impredicative quantification over the universe of propositions.
That is to say that the product of a family of propositions is again a proposition . Thus, a part of this system is impredicative.
CC contains no other primitives. As such, all types must be encoded through impredicative quantification, as in System .
For example, writing for the decoding map of the universe, we can encode the natural numbers by
However, this runs into the usual problem: the defined data types do not have elimination rules/induction principles.
There are two solutions to this:
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}
}
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}
}