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

**Zhaohui Luo**
*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*

Previous |

Index |

Next