A type-theoretic foundation of delimited continuations

Autor: Hugo Herbelin, Zena M. Ariola, Amr Sabry
Přispěvatelé: Department of Computer and Information Science, University of Oregon [Eugene], Logic and computing (LOGICAL), Université Paris-Sud - Paris 11 (UP11)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS), Computer Science Department, Indiana University [Bloomington], Indiana University System-Indiana University System
Rok vydání: 2007
Předmět:
reset
ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic/F.4.1.7: Proof theory
Computer science
Delimited continuation
0102 computer and information sciences
02 engineering and technology
computer.software_genre
01 natural sciences
normalisation
Continuation
store-passing-style
0202 electrical engineering
electronic engineering
information engineering
Calculus
Continuation-passing style
effects
prompt
computer.programming_language
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL]
Programming language
delimited continuations
continuation-passing-style
Classical logic
typing
Subtraction
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
020207 software engineering
shift
16. Peace & justice
Monad (functional programming)
ACM: D.: Software/D.3: PROGRAMMING LANGUAGES/D.3.3: Language Constructs and Features/D.3.3.4: Control structures
Computer Science Applications
ACM: F.: Theory of Computation/F.4: MATHEMATICAL LOGIC AND FORMAL LANGUAGES/F.4.1: Mathematical Logic/F.4.1.2: Lambda calculus and related systems
Variable (computer science)
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
010201 computation theory & mathematics
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
subtraction
Lambda calculus
control
computer
Software
subcontinuation
Zdroj: Higher-Order and Symbolic Computation
Higher-Order and Symbolic Computation, Springer Verlag, 2007
Higher-Order and Symbolic Computation, 2007
ISSN: 1573-0557
1388-3690
Popis: International audience; 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.
Databáze: OpenAIRE
Externí odkaz: