Constructions, inductive types and strong normalization

• Main Author: Altenkirch, Thorsten
• Published: University of Edinburgh 1993
• Subjects: 510
• Online Access: http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.640438

This thesis contains an investigation of Coquand's Calculus of Construction, 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 normalisation 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 normalisation argument can be extended to non-algebraic inductive types. We emphasise that our interpretation is sound for <I>large eliminations</I>, 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 normalisation 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.