Title
Equational axiomatization of call-by-name delimited control
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 Kameyama117117.29
Asami Tanaka231.05