A Type-Theoretic Foundation of Delimited ContinuationsReportar como inadecuado

A Type-Theoretic Foundation of Delimited Continuations - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

1 Department of Computer and Information Science 2 LOGICAL - Logic and computing UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR8623 3 Computer Science Department

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.

Keywords : delimited continuations control prompt reset shift subcontinuation subtraction continuation-passing-style store-passing-style normalisation typing effects

Autor: Zena Ariola - Hugo Herbelin - Amr Sabry -

Fuente: https://hal.archives-ouvertes.fr/


Documentos relacionados