A type-theoretic foundation of continuations and prompts
| Autor: | Hugo Herbelin, Amr Sabry, Zena M. Ariola |
|---|---|
| Rok vydání: | 2004 |
| Předmět: |
Mathematical logic
Delimited continuation Programming language Computer science Classical logic computer.software_genre Monad (functional programming) Computer Graphics and Computer-Aided Design Monadic predicate calculus Operational semantics First-order logic Continuation TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Lambda calculus computer Algorithm Software Logic programming computer.programming_language |
| Zdroj: | ICFP |
| ISSN: | 1558-1160 0362-1340 |
| Popis: | There is a correspondence between classical logic and programming language calculi with first-class continuations. With the addition of control delimiters (prompts), the continuations become composable and the calculi are believed to become more expressive. We formalise that the addition of prompts 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. From a logic perspective, the effect annotations can be understood in a standard logic extended with the dual of implication, namely subtraction. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|