• People
• Events
• Research

CC_{subset}^{infty} and its Meta Theory

Abstract: Extending the Calculus of Constructions with an infinite type hierarchy results in a more powerful system in which abstract mathematics may be adequately formalized. The meta-theory of Constructions with an infinite type hierarchy is studied in this paper. The main result is the strong normalization theorem, which shows the proof-theoretic consistency of the calculus and establishes the theoretical foundation of an implementation.

LFCS report ECS-LFCS-88-58