|
|
VOLUME 3, ISSUE 4, PAPER 12
|
A proof of strong normalisation using domain theory
|
©Thierry Coquand, Chalmers Tekniska Högskola, Gothenburg
©Arnaud Spiwack, LIX, Ecole Polytechnique
|
Abstract
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.
|
Publication date: December 4, 2007
Full Text: PDF | PostScript
DOI: 10.2168/LMCS-3(4:12)2007
Hit Counts: 5118 |
 Creative Commons | |
