Santo, Jose Espirito and Matthes, Ralph and Pinto, Luis - Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi

lmcs:1149 - Logical Methods in Computer Science, May 25, 2009, Volume 5, Issue 2
Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi

Authors: Santo, Jose Espirito and Matthes, Ralph and Pinto, Luis

The intuitionistic fragment of the call-by-name version of Curien and Herbelin's \lambda\_mu\_{\~mu}-calculus is isolated and proved strongly normalising by means of an embedding into the simply-typed lambda-calculus. Our embedding is a continuation-and-garbage-passing style translation, the inspiring idea coming from Ikeda and Nakazawa's translation of Parigot's \lambda\_mu-calculus. The embedding strictly simulates reductions while usual continuation-passing-style transformations erase permutative reduction steps. For our intuitionistic sequent calculus, we even only need "units of garbage" to be passed. We apply the same method to other calculi, namely successive extensions of the simply-typed λ-calculus leading to our intuitionistic system, and already for the simplest extension we consider (λ-calculus with generalised application), this yields the first proof of strong normalisation through a reduction-preserving embedding. The results obtained extend to second and higher-order calculi.


Source : oai:arXiv.org:0903.1822
DOI : 10.2168/LMCS-5(2:11)2009
Volume: Volume 5, Issue 2
Published on: May 25, 2009
Submitted on: February 29, 2008
Keywords: Computer Science - Logic in Computer Science,F.4.1


Share

Consultation statistics

This page has been seen 45 times.
This article's PDF has been downloaded 21 times.