In this text we describe the calculus of constructions as one of the most interesting typed lambda calculus. It is a sweet spot in the design space of typed lambda calculi because it can express an immense set of computable functions and it can express a large set of logical propositions including their proofs.
The paper is written in a textbook style. The needed concepts are introduced step by step and the proofs are layed out sufficiently detailed for newcomers to the subject. The readers who are familiar with basic concepts of lambda calculus and computer science can get a good unterstanding of typed lambda calculus.
pdf