Skip to Main content Skip to Navigation
Journal articles

A Type-Theoretic Foundation of Delimited Continuations

Zena Ariola 1 Hugo Herbelin 2 Amr Sabry 3
2 LOGICAL - Logic and computing
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR8623
Abstract : There is a correspondence between classical logic and programming language calculi with first-class continuations. With the addition of control delimiters, the continuations become composable and the calculi become more expressive. We present a fine-grained analysis of control delimiters and formalise that their addition corresponds to the addition of a single dynamically-scoped variable modelling the special top-level continuation. From a type perspective, the dynamically-scoped variable requires effect annotations. In the presence of control, the dynamically-scoped variable can be interpreted in a purely functional way by applying a store-passing style. At the type level, the effect annotations are mapped within standard classical logic extended with the dual of implication, namely subtraction. A continuation-passing-style transformation of lambda-calculus with control and subtraction is defined. Combining the translations provides a decomposition of standard CPS transformations for delimited continuations. Incidentally, we also give a direct normalisation proof of the simply-typed lambda-calculus with control and subtraction.
Complete list of metadata

Cited literature [54 references]  Display  Hide  Download

https://hal.inria.fr/inria-00177326
Contributor : Hugo Herbelin <>
Submitted on : Sunday, October 7, 2007 - 4:53:56 PM
Last modification on : Wednesday, September 16, 2020 - 4:56:12 PM
Long-term archiving on: : Sunday, April 11, 2010 - 10:22:31 PM

Files

hosc-AriHerSab07-delim-cont.pd...
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00177326, version 1

Collections

Citation

Zena Ariola, Hugo Herbelin, Amr Sabry. A Type-Theoretic Foundation of Delimited Continuations. Higher-Order and Symbolic Computation, Springer Verlag, 2007. ⟨inria-00177326⟩

Share

Metrics

Record views

441

Files downloads

439