The calculus of constructions (CoC) is a higher-order typed lambda calculus where types are first-class values. It is thus possible, within the CoC, to define functions from, say, integers to types, types to types as well as functions from integers to integers. The CoC is strongly normalizing. Typed versions of the lambda calculus extend the standard lambda calculus with types. ... Type has historically had the following uses: In biology, a type is the specimen or specimens upon which an original species description is based. ... In computing, a first-class object (also -value, -entity, -citizen), in the context of a particular programming language, is an entity which can be used in programs without restriction (when compared to other kinds of objects in the same language). ... In mathematical logic and theoretical computer science, a rewrite system has the normalization property if every term is strongly normalizing; that is, if every sequence of rewrites eventually terminates to a term in normal form. ...

The CoC was initially developed by Thierry Coquand.

The CoC was the basis of the early versions of the Coq theorem prover; later versions were built upon the Calculus of Inductive Constructions an extension of CoC with native support for inductive datatypes. In the original CoC, inductive datatypes had to be emulated as their polymorphic destructor function. In automated theorem proving, Coq is a proof assistant which handles mathematical assertions, checks mechanically proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification. ... On computer science, a datatype (often simply type) is a name or label for a set of values and some operations which can be performed on that set of values. ...

The basics of the calculus of constructions

The Calculus of Constructions can be considered an extension of the Curry-Howard isomorphism. The Curry-Howard isomorphism associates a term in the simply typed lambda calculus with each natural-deduction proof in intuitionistic propositional logic. The Calculus of Constructions extends this isomorphism to proofs in the full intuitionistic predicate calculus, which includes proofs of quantified statements (which we will also call "propositions"). The Curry-Howard correspondence is the close relationship between computer programs and mathematical proofs; the correspondence is also known as the Curry-Howard isomorphism, or the formulae-as-types correspondence. ... Typed versions of the lambda calculus extend the standard lambda calculus with types. ... Intuitionistic logic, or constructivist logic, is the logic used in mathematical intuitionism and other forms of mathematical constructivism. ...

Terms

A term in the calculus of constructions is constructed using the following rules:

• T is a term (also called Type)
• P is a term (also called Prop, the type of all propositions)
• If A and B are terms, then so are
  • ()
  • ()

The calculus of constructions has 4 types of objects:

1. proofs, which are terms whose types are propositions
2. propositions, which are also known as small types
3. predicates, which are functions that return propositions
4. large types, which are the types of predicates. (P is an example of a large type)
5. T itself, which is the type of large types.

Judgements

In the calculus of constructions, a judgement is a typing inference:

Which can be read as the implication

If variables have types , then term has type .

The valid judgements 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 , and we use K to mean either P or T. We will write A:B:C to mean "A has type B, and B has type C". We will write B(x: = N) to mean the result of substituting the term N for the variable x in the term B.

An inference rule is written in the form

which means

If is a valid judgement, then so is

Inference rules for calculus of constructions

Defining logical operators

The calculus of constructions is very parsimonious when it comes to 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 A + B 

See also

• Lambda calculus
• Typed lambda calculus
• Curry-Howard isomorphism
• Intuitionistic logic
• Intuitionistic Type Theory
• Jean-Yves Girard
• Thierry Coquand
• System F