Axiomatizing Subtyped Delimited Continuations
Marek Materzok · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2013
We present direct equational axiomatizations of the call-by-value lambda calculus with the control operators shift_0 and reset_0 that generalize Danvy and Filinski's shift and reset in that they allow for abstracting control beyond the top-most delimited continuation. We address an untyped version of the calculus as well as a typed version with effect subtyping. For each of the calculi we present a set of axioms that we prove sound and complete with respect to the corresponding CPS translation.