Strong normalisation of cut-elimination that simulates β-reduction

Kentaro Kikuchi, Stéphane Lengrand

Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish
Title of host publicationFoundations 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
Pages380-394
Number of pages15
DOIs
Publication statusPublished - 2008
Event"11th International Conferenceon the Foundations of Software Science and Computations Structures, FOSSACS 2008" - Budapest, Hungary
Duration: 2008 Mar 292008 Apr 6

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4962 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/TerritoryHungary
CityBudapest
Period08/3/2908/4/6

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Strong normalisation of cut-elimination that simulates β-reduction'. Together they form a unique fingerprint.

Cite this