A Proof of Strong Normalisation using Domain Theory

Thierry Coquand 1 Arnaud Spiwack 2, 3
3 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : U. Berger, significantly simplified Tait's normalisation proof for bar recursion, replacing Tait's introduction of infinite terms by the construction of a domain having the property that a term is strongly normalizing if its semantics is not bottom. The goal of this paper is to show that, using ideas from the theory of intersection types and Martin-Löf's domain interpretation of type theory, we can in turn simplify U. Berger's argument in the construction of such a domain model. We think that our domain model can be used to give modular proofs of strong normalization for various type theory. As an example, we show in some details how it can be used to prove strong normalization for Martin-Löf dependent type theory extended with bar recursion, and with some form of proof-irrelevance.
Type de document :
Communication dans un congrès
LICS 2006, Aug 2006, Seatle, United States. 10 p., 2006, 〈10.1109/LICS.2006.8〉
Liste complète des métadonnées

Littérature citée [24 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00432490
Contributeur : Arnaud Spiwack <>
Soumis le : lundi 16 novembre 2009 - 15:34:23
Dernière modification le : jeudi 10 mai 2018 - 02:06:34
Document(s) archivé(s) le : jeudi 17 juin 2010 - 20:30:20

Fichier

sn2.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Thierry Coquand, Arnaud Spiwack. A Proof of Strong Normalisation using Domain Theory. LICS 2006, Aug 2006, Seatle, United States. 10 p., 2006, 〈10.1109/LICS.2006.8〉. 〈inria-00432490〉

Partager

Métriques

Consultations de la notice

199

Téléchargements de fichiers

113