Strong normalisation of cut-elimination that simulates β-reduction

Kentaro Kikuchi; Stéphane Lengrand

doi:10.1007/978-3-540-78499-9_27

Strong normalisation of cut-elimination that simulates β-reduction

Kentaro Kikuchi, Stéphane Lengrand

Systems & Software Division

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

2 Citations (Scopus)

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.

Original language	English
Title of host publication	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
Pages	380-394
Number of pages	15
DOIs	https://doi.org/10.1007/978-3-540-78499-9_27
Publication status	Published - 2008
Event	"11th International Conferenceon the Foundations of Software Science and Computations Structures, FOSSACS 2008" - Budapest, Hungary Duration: 2008 Mar 29 → 2008 Apr 6

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	4962 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	"11th International Conferenceon the Foundations of Software Science and Computations Structures, FOSSACS 2008"
Country/Territory	Hungary
City	Budapest
Period	08/3/29 → 08/4/6

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/978-3-540-78499-9_27

Cite this

Kikuchi, K., & Lengrand, S. (2008). Strong normalisation of cut-elimination that simulates β-reduction. In 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 (pp. 380-394). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4962 LNCS). https://doi.org/10.1007/978-3-540-78499-9_27

Strong normalisation of cut-elimination that simulates β-reduction. / Kikuchi, Kentaro; Lengrand, Stéphane.

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. 2008. p. 380-394 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4962 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Kikuchi, K & Lengrand, S 2008, Strong normalisation of cut-elimination that simulates β-reduction. in 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. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4962 LNCS, pp. 380-394, "11th International Conferenceon the Foundations of Software Science and Computations Structures, FOSSACS 2008", Budapest, Hungary, 08/3/29. https://doi.org/10.1007/978-3-540-78499-9_27

Kikuchi K, Lengrand S. Strong normalisation of cut-elimination that simulates β-reduction. In 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. 2008. p. 380-394. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-540-78499-9_27

Kikuchi, Kentaro ; Lengrand, Stéphane. / Strong normalisation of cut-elimination that simulates β-reduction. 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. 2008. pp. 380-394 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{ca4a6bab337b48d9b7936ce26e1bbc01,

title = "Strong normalisation of cut-elimination that simulates β-reduction",

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.",

author = "Kentaro Kikuchi and St{\'e}phane Lengrand",

year = "2008",

doi = "10.1007/978-3-540-78499-9_27",

language = "English",

isbn = "3540784977",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "380--394",

booktitle = "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",

note = "{"}11th International Conferenceon the Foundations of Software Science and Computations Structures, FOSSACS 2008{"} ; Conference date: 29-03-2008 Through 06-04-2008",

}

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 -

Strong normalisation of cut-elimination that simulates β-reduction

Abstract

Publication series

Other

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this