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...

• Type: Journal
• Year: 2010
• Where: PPDP
• Authors: Yukiyoshi Kameyama, Asami Tanaka
• Keywords: Control Operators, Delimited, Keywords Control Operators, PPDP 2010, Programming Languages