CC_{subset}^{infty} and its Meta Theory
Zhaohui LuoAbstract: 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.
Previous | Index | Next