Computer Science – Logic in Computer Science
Scientific paper
2009-03-10
LMCS 5 (2:11) 2009
Computer Science
Logic in Computer Science
Scientific paper
10.2168/LMCS-5(2:11)2009
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.
Matthes Ralph
Pinto Luis
Santo Jose Espirito
No associations
LandOfFree
Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-187545