Equational axiomatization of call-by-name delimited control

11 years 8 months ago
Equational axiomatization of call-by-name delimited control
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 use the linearity of certain variables in the CPS terms, and (2) we must distinguish continuation variables from ordinary variables in the source terms. We also show that our axiomatization holds for the typed calculus. Categories and Subject Descriptors D.3.1 [Programming Languages]: Formal Definitions and...
Yukiyoshi Kameyama, Asami Tanaka
Added 29 Jan 2011
Updated 29 Jan 2011
Type Journal
Year 2010
Where PPDP
Authors Yukiyoshi Kameyama, Asami Tanaka
Comments (0)