eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2013-09-02
395
414
10.4230/LIPIcs.CSL.2013.395
article
Proving Strong Normalisation via Non-deterministic Translations into Klop's Extended lambda-Calculus
Kikuchi, Kentaro
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol023-csl2013/LIPIcs.CSL.2013.395/LIPIcs.CSL.2013.395.pdf
Strong normalisation
Klop's extended lambda-calculus
Explicit substitution
Cut-elimination