A proof of strong normalisation using domain theory

TL;DR

This paper simplifies the proof of strong normalisation for type theories by building a domain model using intersection types and Martin-Löf's interpretation, extending Berger's work to dependent type theory.

Contribution

It introduces a new domain model that simplifies Berger's proof and applies it to Martin-Löf's dependent type theory with Spector double negation shift.

Findings

Simplified proof of strong normalisation using domain theory.

Constructed a domain model for untyped and typed terms.

Extended the proof to Martin-Löf's dependent type theory.

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\"{o}f dependent type theory extended with a program for Spector double negation shift.