*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)*