An Extended Calculus of Constructions

Zhaohui Luo

Abstract: This thesis presents and studies a unifying thoery of dependent types ECC - Extended Calculus of Constructions. ECC integrates Coquand-Huet's (impredicative) calculus of constructions and Martin-Löf's (predicative) type theory with universes, and turns out to be a strong and expressive calculus for formalization of mathematics, structured proof development and program specification.

The meta-theory of ECC is studied and we show that the calculus has good meta-theoretic properties. The main proof-theoretic result is the strong normalization theorem, proved by using Girard-Tait's reducibility method based on a quasi normalization theorem which makes explicit the predicativity of the predicative universes. The strong normalization result shows the proof-theoretic consistency of the calculus; in particular, it implies the consistency of the embedded intuitionistic higher-order logic and the decidability of the theory. The meta-theoretic results establish the theoretical foundations both for pragmatic applications in theorem-proving and program specification and for computer implementations of the theory. ECC has been implemented in the proof development system LEGO developed by Pollack.

In ECC, dependent Sigma-types are non-propositional types residing in the predicative universes and propositions are lifted as higher-level types as well. This solves the known difficulty that adding strong Sigma-types to an impredicative system results in logical paradox and enables Sigma-types to be used to express the intuitionistic notion of subsets. Sigma-types together with type universes hence provide useful abstraction and module mechanisms for abstract description of mathematical theories and basic mechanisms for program specification and adequate formalization of abstract mathematics e.g. abstract algebras and notions in category theory). A notion of (abstract) mathematical theory can be described and leads to a promising approach to abstract reasoning and structured reasoning. Program specifications can be expressed by Sigma-types, using propositions in the embedded logic to describe program properties (for example, by an equality reflection result, computational equality can be modeled by the propositional Leibniz's equality definable in the theory). These developments allow comprehensive structuring of formal or rigorous development of proofs and programs.

Also discussed is how the calculus can be understood set-theoretically. We explain an omega-Set (realizability) model of the theory. In particular, propositions can be interpreted as partial equivalence relations and the predicative type universes as corresponding to large set universes.
PhD thesis - Price £8.00

LFCS report ECS-LFCS-90-118 (also published as CST-65-90)

Previous | Index | Next