some image logo

HOME

SEARCH

CURRENT ISSUE

REGULAR ISSUES

   Volume 1 (2005)

   Volume 2 (2006)

   Volume 3 (2007)

   Volume 4 (2008)

   Volume 5 (2009)

      Issue 1

      Issue 2

      Issue 3

      Issue 4

   Volume 6 (2010)

   Volume 7 (2011)

   Volume 8 (2012)

   Volume 9 (2013)

   Volume 10 (2014)

   Volume 11 (2015)

   Volume 12 (2016)

   Volume 13 (2017)

SPECIAL ISSUES

SURVEY ARTICLES

AUTHORS

ABOUT

SERVICE

LOGIN

FAQ

SUPPORT

CONTACT

VOLUME 5, ISSUE 2, PAPER 11


Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi

©Jose Espirito Santo, Departamento de Matemática, Universidade do Minho
©Ralph Matthes, Institut de Recherche en Informatique de Toulouse (IRIT), C.N.R.S. and Universit
©Luis Pinto, Departamento de Matemática, Universidade do Minho

Abstract
The intuitionistic fragment of the call-by-name version of Curien and Herbelin's λ--μ-μ~-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 λ-μ-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.

Publication date: May 25, 2009

Full Text: PDF | PostScript
DOI: 10.2168/LMCS-5(2:11)2009

Hit Counts: 9069

Creative Commons