Calculus of Inductive Constructions

The Calculus of Inductive Constructions (CIC) is a type theory. It extends the calculus of constructions (CC) with inductive definitions. It is the theoretical basis of the Coq proof assistant.

Motivation

While CC can represent inductive types using impredicative quantification and Church encodings, that representation is neither efficient nor sufficiently logically strong.

References

There is a tutorial presentation of CIC in

Paulin-Mohring, Christine. 2015. ‘Introduction to the Calculus of Inductive Constructions’. In All about Proofs, Proofs for All, edited by Bruno Woltzenlogel Paleo and David Delahaye. Vol. 55. Studies in Logic (Mathematical Logic and Foundations). College Publications. https://hal.inria.fr/hal-01094195.

@incollection{paulin-mohring_2015,
	series = {Studies in {Logic} ({Mathematical} logic and foundations)},
	title = {Introduction to the {Calculus} of {Inductive} {Constructions}},
	volume = {55},
	url = {https://hal.inria.fr/hal-01094195},
	booktitle = {All about {Proofs}, {Proofs} for {All}},
	publisher = {College Publications},
	author = {Paulin-Mohring, Christine},
	editor = {Paleo, Bruno Woltzenlogel and Delahaye, David},
	year = {2015},
}

CIC itself was introduced in the following two papers.

Coquand, Thierry, and Christine Paulin. 1990. ‘Inductively Defined Types’. In COLOG-88, edited by Per Martin-Löf and Grigori Mints, 417:50–66. Lecture Notes in Computer Science. Berlin, Heidelberg: Springer Berlin Heidelberg. https://doi.org/10.1007/3-540-52335-9_47.

@inproceedings{coquand_1990,
	address = {Berlin, Heidelberg},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Inductively defined types},
	volume = {417},
	doi = {10.1007/3-540-52335-9_47},
	booktitle = {{COLOG}-88},
	publisher = {Springer Berlin Heidelberg},
	author = {Coquand, Thierry and Paulin, Christine},
	editor = {Martin-Löf, Per and Mints, Grigori},
	year = {1990},
	pages = {50--66}
}

Paulin-Mohring, Christine. 1993. ‘Inductive Definitions in the System Coq Rules and Properties’. In Typed Lambda Calculi and Applications, edited by Marc Bezem and Jan Friso Groote, 664:328–45. Lecture Notes in Computer Science. Berlin/Heidelberg: Springer-Verlag. https://doi.org/10.1007/BFb0037116.


@inproceedings{bezem_inductive_1993,
	address = {Berlin/Heidelberg},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Inductive definitions in the system {Coq} rules and properties},
	volume = {664},
	doi = {10.1007/BFb0037116},
	booktitle = {Typed {Lambda} {Calculi} and {Applications}},
	publisher = {Springer-Verlag},
	author = {Paulin-Mohring, Christine},
	editor = {Bezem, Marc and Groote, Jan Friso},
	year = {1993},
	pages = {328--345}
}