Chapter 4: The Calculus of Inductive Constructions
The underlying formal language of Coq is the Calculus of (Co)Inductive Constructions(Cic in short). It is presented in this chapter.In Cic all objects have a type. There are types for functions (or programs), there are atomic types (especially datatypes)... but also types for proofs and types for the types themselves. Especially, any object handled in the formalism must belong to a type. For instance, the statement ``for all x, P'' is not allowed in type theory; you must say instead: ``for all x belonging to T, P''. The expression ``x belonging to T'' is written ``x:T''. One also says: ``x has type T''. The terms of Cic are detailed in section 4.1.
In Cic there is an internal reduction mechanism. In particular, it allows to decide if two programs are intentionally equal (one says convertible). Convertibility is presented in section 4.3.
The remaining sections are concerned with the type-checking of terms. The beginner can skip them.
The reader seeking a background on the Cic may read several papers. Giménez [48] provides an introduction to inductive and coinductive definitions in Coq, Werner [98] and Paulin-Mohring [87] are the most recent theses on the Cic. Coquand-Huet [22, 23, 24] introduces the Calculus of Constructions. Coquand-Paulin [25] introduces inductive definitions. The Cic is a formulation of type theory including the possibility of inductive constructions. Barendregt [5] studies the modern form of type theory.
- 4.1 The terms
- 4.2 Typed terms
- 4.3 Conversion rules
- 4.4 Definitions in environments
- 4.5 Inductive Definitions
- 4.6 Coinductive types