Extending the Calculus of Constructions with Type:Type

The Calculus of Constructions is a higher-order formalism for writing constructive proofs in a natural deduction style, inspired from work of de Bruijn, Girard and Martin-Löf. The calculus and its syntactic theory were presented in Coquand’s thesis, and an implementation by the author was used to mechanically verify a substantial number of proofs demonstrating the power of expression of the formalism. The Calculus of Constructions is proposed as a foundation for the design of programming environments where programs are developed consistently with formal specifications.