TY - GEN
T1 - Strong normalisation of cut-elimination that simulates β-reduction
AU - Kikuchi, Kentaro
AU - Lengrand, Stéphane
PY - 2008
Y1 - 2008
N2 - This paper is concerned with strong normalisation of cut-elimination for a standard intuitionistic sequent calculus. The cut- elimination procedure is based on a rewrite system for proof-terms with cut-permutation rules allowing the simulation of β-reduction. Strong normalisation of the typed terms is inferred from that of the simply-typed λ-calculus, using the notions of safe and minimal reductions as well as a simulation in Nederpelt-Klop's λI-calculus. It is also shown that the type-free terms enjoy the preservation of strong normalisation (PSN) property with respect to β-reduction in an isomorphic image of the type-free λ-calculus.
AB - This paper is concerned with strong normalisation of cut-elimination for a standard intuitionistic sequent calculus. The cut- elimination procedure is based on a rewrite system for proof-terms with cut-permutation rules allowing the simulation of β-reduction. Strong normalisation of the typed terms is inferred from that of the simply-typed λ-calculus, using the notions of safe and minimal reductions as well as a simulation in Nederpelt-Klop's λI-calculus. It is also shown that the type-free terms enjoy the preservation of strong normalisation (PSN) property with respect to β-reduction in an isomorphic image of the type-free λ-calculus.
UR - http://www.scopus.com/inward/record.url?scp=47249090084&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=47249090084&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-78499-9_27
DO - 10.1007/978-3-540-78499-9_27
M3 - Conference contribution
AN - SCOPUS:47249090084
SN - 3540784977
SN - 9783540784975
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 380
EP - 394
BT - Foundations of Software Science and Computational Structures - 11th Int. Conf., FOSSACS 2008 - Held as Part of the Joint European Conf. on Theory and Practice of Software, ETAPS 2008, Proceedings
T2 - "11th International Conferenceon the Foundations of Software Science and Computations Structures, FOSSACS 2008"
Y2 - 29 March 2008 through 6 April 2008
ER -