Proving strong normalisation via non-deterministic translations into Klop's extended λ-calculus

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

In this paper we present strong normalisation proofs using a technique of non-deterministic translations into Klop's extended λ-calculus. We first illustrate the technique by showing strong normalisation of a typed calculus that corresponds to natural deduction with general elimination rules. Then we study its explicit substitution version, the type-free calculus of which does not satisfy PSN with respect to reduction of the original calculus; nevertheless it is shown that typed terms are strongly normalising with respect to reduction of the explicit substitution calculus. In the same framework we prove strong normalisation of Sørensen and Urzyczyn's cut-elimination system in intuitionistic sequent calculus.

Original languageEnglish
Title of host publicationLeibniz International Proceedings in Informatics, LIPIcs
EditorsSimona Ronchi Della Rocca
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Pages395-414
Number of pages20
ISBN (Electronic)9783939897606
DOIs
Publication statusPublished - 2013 Sep 1
Event22nd Annual Conference of the European Association for Computer Science Logic EACSL, CSL 2013 - Torino, Italy
Duration: 2013 Sep 22013 Sep 5

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume23
ISSN (Print)1868-8969

Other

Other22nd Annual Conference of the European Association for Computer Science Logic EACSL, CSL 2013
Country/TerritoryItaly
CityTorino
Period13/9/213/9/5

Keywords

  • Cut-elimination
  • Explicit substitution
  • Klop's extended λ-calculus
  • Strong normalisation

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'Proving strong normalisation via non-deterministic translations into Klop's extended λ-calculus'. Together they form a unique fingerprint.

Cite this