Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH scholarly article en Kikuchi, Kentaro http://www.dagstuhl.de/lipics License
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-42108
URL:

Proving Strong Normalisation via Non-deterministic Translations into Klop's Extended lambda-Calculus

pdf-format:


Abstract

In this paper we present strong normalisation proofs using a technique of non-deterministic translations into Klop's extended lambda-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.

BibTeX - Entry

@InProceedings{kikuchi:LIPIcs:2013:4210,
  author =	{Kentaro Kikuchi},
  title =	{{Proving Strong Normalisation via Non-deterministic Translations into Klop's Extended lambda-Calculus}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{395--414},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Simona Ronchi Della Rocca},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2013/4210},
  URN =		{urn:nbn:de:0030-drops-42108},
  doi =		{10.4230/LIPIcs.CSL.2013.395},
  annote =	{Keywords: Strong normalisation, Klop's extended lambda-calculus, Explicit substitution, Cut-elimination}
}

Keywords: Strong normalisation, Klop's extended lambda-calculus, Explicit substitution, Cut-elimination
Seminar: Computer Science Logic 2013 (CSL 2013)
Issue date: 2013
Date of publication: 2013


DROPS-Home | Fulltext Search | Imprint Published by LZI