The Extended Calculus of Constructions
Luo, Zhaohui · 1994
Abstract The Extended Calculus of Constructions (ECC) is a type theory which is developed as an initial step towards a rich computational language with a powerful internal logic for modular development of programs, specifications, and proofs. The basic ideas incorporated in ECC, in particular, the idea that there should be a conceptual distinction between the notions of logical proposition and data type, have been explained in the Introduction. It is also based on those ideas that the study of ECC will lead to a unifying theory of dependent types which unifies Martin-Leif’s type theory with universes [ML75, ML84] and Coquand-Huet’s calculus of constructions [CH88] (see Chapter 9).