## Constructions, Inductive Types and Strong Normalization

**Thorsten Altenkirch**
*Abstract:* This thesis contains an investigation of
Coquand's Calculus of Constructions, a basic impredicative Type
Theory. We review syntactic properties of the calculus, in
particular decidability of equality and type-checking, based on the
equality-as-judgement presentation. We present a set-theoretic
notion of model, CC-structures, and use this to give a new strong
normalization proof based on a modification of the realizability
interpretation. An extension of the core calculus by inductive
types is investigated and we show, using the example of infinite
trees, how the realizability semantics and the strong normalization
argument can be extended to non-algebraic inductive types. We
emphasize that our interpretation is sound for *large
eliminations*, e.g. allows the definition of sets by recursion.
Finally we apply the extended calculus to a non-trivial problem:
the formalization of the strong normalization argument for Girard's
System F. This formal proof has been developed and checked using
the LEGO system, which has been implemented by Randy Pollack. We
include the LEGO files in the appendix.

**PhD thesis - Price £8.00**

*LFCS report ECS-LFCS-93-279 (also published as
CST-106-93)*

Previous |

Index |

Next