Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1145/1016850.1016860 | Proceedings of the ninth ACM SIGPLAN international conference on Functional programming |
Keywords | Field | DocType |
continuation,classical logic,monad,programming language,subtraction | Lambda calculus,Programming language,Delimited continuation,Computer science,Continuation,First-order logic,Classical logic,Logic programming,Monadic predicate calculus,Monad (functional programming) | Conference |
Volume | Issue | ISSN |
39 | 9 | 0362-1340 |
ISBN | Citations | PageRank |
1-58113-905-5 | 18 | 0.81 |
References | Authors | |
29 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Zena M. Ariola | 1 | 482 | 38.61 |
| Hugo Herbelin | 2 | 435 | 30.00 |
| Amr Sabry | 3 | 520 | 35.46 |