Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi

DOI10.1007/978-3-540-73228-0_11MaRDI QIDQ5901474zbMATH OpenOpenAlexFDO

Authors José Espírito Santo, Ralph Matthes, Luís Pinto

Publication date 10 March 2009

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/0903.1822

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Cut-elimination and normal-form theorems (03F05) Functional programming and lambda calculus (68N18)

Abstract: 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.

Recommendations

• Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi
• Call-by-value, call-by-name, and strong normalization for the classical sequent calculus
• scientific article; zbMATH DE number 1722662
• Confluency and strong normalizability of call-by-value \(\lambda \mu\)-calculus
• Monadic translation of classical sequent calculus

Cited in

(5)

• Continuation-passing style models complete for intuitionistic logic
• Monadic Translation of Intuitionistic Sequent Calculus
• Monadic translation of classical sequent calculus
• Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi
• Strong normalization proofs by CPS-translations

This page was built for publication: Continuation-Passing Style and Strong Normalisation for Intuitionistic Sequent Calculi

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5901474)