Paper: Proof of strong normalisation using domain theory (at LICS 2006)

Authors: Thierry Coquand Arnaud Spiwack

Abstract

U. Bergel; [ I I ] signijicantly simplijied Tait's normalisation proof for bar recursion [27], see also [9], replacing Tait's introduction of injinite terms by the construction of a domain having the property that a term is strongly normalizing if its semantics is \ne. The goal of this paper is to show that, using ideas from the theory of intersection types [2, 6, 7, 211 and Martin-Liif's domain interpretation of type theory [18], 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-Liif dependent type theory extended with bar recursion, and with some form ofproof-irrelevance.

BibTeX

  @InProceedings{CoquandSpiwack-Proofofstrongnormal,
    author = 	 {Thierry Coquand and Arnaud Spiwack},
    title = 	 {Proof of strong normalisation using domain theory},
    booktitle =  {Proceedings of the Twenty-First Annual IEEE Symposium on Logic in Computer Science (LICS 2006)},
    year =	 {2006},
    month =	 {August}, 
    pages =      {307--316},
    location =   {Seattle, Washington, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }