A higher-order calculus and theory abstraction
Zhaohui Luo · Information and Computation · 1991
We present a higher-order calculus ECC which naturally combines Coquand-Huet's calculus of constructions and Martin-Löf's type theory with universes. ECC is very expressive, both for structured abstract reasoning and for program specification and construction. In particular, the strong sum types together with the type universes provide a useful module mechanism for abstract description of mathematical theories and adequate formalization of abstract mathematics. This allows comprehensive structuring of interactive development of specifications, programs and proofs. After a summary of the meta-theoretic properties of the calculus, an ω-Set (realizability) model of ECC is described to show how its essential properties can be captured set-theoretically. The model construction entails the logical consistency of the calculus and gives some hints on how to adequately formalize abstract mathematics. Theory abstraction in ECC is discussed as a pragmatic application.