Abstract
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. © 2008 Springer-Verlag Berlin Heidelberg.
Cite
CITATION STYLE
Kikuchi, K., & Lengrand, S. (2008). Strong normalisation of cut-elimination that simulates β-reduction. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4962 LNCS, pp. 380–394). https://doi.org/10.1007/978-3-540-78499-9_27
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
