Some of its variants include the calculus of inductive constructions[1] (which adds
inductive types), the calculus of (co)inductive constructions (which adds
coinduction), and the predicative calculus of inductive constructions (which removes some
impredicativity).
General traits
The CoC is a higher-order
typed lambda calculus, initially developed by
Thierry Coquand. It is well known for being at the top of
Barendregt's
lambda cube. It is possible within CoC to define functions from terms to terms, as well as terms to types, types to types, and types to terms.
The CoC has been developed alongside the
Coqproof assistant. As features were added (or possible liabilities removed) to the theory, they became available in Coq.
Variants of the CoC are used in other proof assistants, such as
Matita and
Lean.
The calculus of constructions has five kinds of objects:
proofs, which are terms whose types are propositions;
propositions, which are also known as small types;
predicates, which are functions that return propositions;
large types, which are the types of predicates ( is an example of a large type);
itself, which is the type of large types.
Judgments
The calculus of constructions allows proving typing judgments:
,
which can be read as the implication
If variables have, respectively, types , then term has type .
The valid judgments for the calculus of constructions are derivable from a set of inference rules. In the following, we use to mean a sequence of type assignments
; to mean terms; and to mean either or . We shall write to mean the result of substituting the term for the
free variable in the term .
An inference rule is written in the form
,
which means
if is a valid judgment, then so is .
Inference rules for the calculus of constructions
1.
2.
3.
4.
5.
6.
Defining logical operators
The calculus of constructions has very few basic operators: the only logical operator for forming propositions is . However, this one operator is sufficient to define all the other logical operators:
Defining data types
The basic data types used in computer science can be defined within the calculus of constructions:
Booleans
Naturals
Product
Disjoint union
Note that Booleans and Naturals are defined in the same way as in
Church encoding. However, additional problems arise from propositional extensionality and proof irrelevance.[3]
Also available freely accessible online: Coquand, Thierry; Huet, Gérard (1986).
The calculus of constructions (Technical report).
INRIA, Centre de Rocquencourt. 530. Note terminology is rather different. For instance, () is written [x : A] B.