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.
Type de document :
Article dans une revue
Higher-Order and Symbolic Computation, Springer Verlag, 2007
Liste complète des métadonnées

Littérature citée [54 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00177326
Contributeur : Hugo Herbelin <>
Soumis le : dimanche 7 octobre 2007 - 16:53:56
Dernière modification le : jeudi 10 mai 2018 - 01:05:46
Document(s) archivé(s) le : dimanche 11 avril 2010 - 22:22:31

Fichiers

hosc-AriHerSab07-delim-cont.pd...
Fichiers produits par l'(les) auteur(s)

Identifiants

  • 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〉

Partager

Métriques

Consultations de la notice

293

Téléchargements de fichiers

173