Paper Info
Title
Continuation-passing style and strong normalisation for intuitionistic sequent calculi
Abstract
The intuitionistic fragment of the call-by-name version of Curien and Herbelin's ‚"~"-calculus is isolated and proved strongly nor- malising by means of an embedding into the simply-typed ‚-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 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 con- sider (‚-calculus with generalised application), this yields the flrst proof of strong normalisation through a reduction-preserving embedding.
Year
DOI
Venue
2007
10.2168/LMCS-5(2:11)2009
Typed Lambda Calculus and Applications
Keywords
Field
DocType
simplest extension,generalised application,call-by-name version,reduction-preserving embedding,intuitionistic fragment,strong normalisation,permutative reduction step,continuation-and-garbage-passing style translation,continuation-passing style,intuitionistic system,inspiring idea,intuitionistic sequent calculus,sequent calculus,continuation passing style
Discrete mathematics,Embedding,Natural deduction,Sequent calculus,Critical pair,Sequent,Cut-elimination theorem,Continuation-passing style,Calculus,Mathematics
Conference
Volume
Issue
ISSN
5
2
Logical Methods in Computer Science, Volume 5, Issue 2 (May 25, 2009) lmcs:1149
Citations 
PageRank 
References 
6
0.52
27
Authors
3
Name
Order
Citations
PageRank
José Espírito Santo16210.79
Ralph Matthes220121.67
Luís Pinto3855.32