Proving Strong Normalisation via Non-deterministic Translations into Klop's Extended lambda-Calculus
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.
Strong normalisation
Klop's extended lambda-calculus
Explicit substitution
Cut-elimination
395-414
Regular Paper
Kentaro
Kikuchi
Kentaro Kikuchi
10.4230/LIPIcs.CSL.2013.395
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode