THE CALCULUS OF CONSTRUCTIONS

The calculus of constructions is a higher-order formalism for constructive proofs in natural deduction style. Every proof is a lambda -expression, typed with propositions of the underlying logic. By removing types we get a pure lambda -expression, expressing its associated algorithm. Computing this lambda -expression corresponds roughly to cut-elimination. It is our thesis that the Curry-Howard correspondence between propositions and types is a powerful paradigm for computer science. In the case of constructions, we obtain the notion of very high-level functioning programming language, with complex polymorphism well-suited for module specification. The notion of type encompasses the usual notion of date type, but allows as well arbitrarily complex algorithmic specifications. We develop the basic theory of a calculus of constructions, and prove a strong normalization theorem showing that all computations terminate. Finally, we suggest various extensions to stronger calculi.