Coquand, Thierry and Spiwack, Arnaud - A proof of strong normalisation using domain theory

lmcs:1099 - Logical Methods in Computer Science, December 4, 2007, Volume 3, Issue 4
A proof of strong normalisation using domain theory

Authors: Coquand, Thierry and Spiwack, Arnaud

Ulrich Berger presented a powerful proof of strong normalisation using domains, in particular it simplifies significantly Tait's proof of strong normalisation of Spector's bar recursion. The main contribution of this paper is to show that, using ideas from intersection types and Martin-Lof's domain interpretation of type theory one can in turn simplify further U. Berger's argument. We build a domain model for an untyped programming language where U. Berger has an interpretation only for typed terms or alternatively has an interpretation for untyped terms but need an extra condition to deduce strong normalisation. As a main application, we show that Martin-Löf dependent type theory extended with a program for Spector double negation shift.


Source : oai:arXiv.org:0709.1401
DOI : 10.2168/LMCS-3(4:12)2007
Volume: Volume 3, Issue 4
Published on: December 4, 2007
Submitted on: March 4, 2007
Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages,F.4.1


Share

Consultation statistics

This page has been seen 70 times.
This article's PDF has been downloaded 15 times.