Abstract | ||
---|---|---|
Control operators for delimited continuations are useful in various fields such as partial evaluation, CPS translation, and representation of monadic effects. While many works in the literature study them in call-by-value, several recent works have shown call-by-name delimited control operators are also worth studying. In this paper, we study semantic foundation of the call-by-name variant of the delimited-control operators "shift" and "reset". In particular, we give a set of direct-style equations as axioms for them, and prove that it is sound and complete with respect to the CPS translation by Biernacka and Biernacki. The key observations in our proof are (1) we need to carefully treat linearity of certain variables in the CPS terms, and (2) we must distinguish continuation variables from ordinary variables. We also mention that our axioms can be used for typed calculus. |
Year | DOI | Venue |
---|---|---|
2010 | 10.1145/1836089.1836100 | Proceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming |
Keywords | Field | DocType |
partial evaluation,call by name,delimited continuation | Evaluation strategy,Programming language,Partial evaluation,Computer science,Delimited continuation,Axiom,Continuation,Algorithm,Operator (computer programming),Calculus,Monad (functional programming) | Conference |
Citations | PageRank | References |
2 | 0.36 | 10 |
Authors | ||
2 |
Name | Order | Citations | PageRank |
---|---|---|---|
Yukiyoshi Kameyama | 1 | 171 | 17.29 |
Asami Tanaka | 2 | 3 | 1.05 |