Reflecting Stacked Continuations in a Fine-Grained Direct-Style Reduction Theory
Dariusz Biernacki, Mateusz Pyzik, Filip Sieczkowski · 2021
The delimited-control operator shift0 has been formally shown to capture the operational semantics of deep handlers for algebraic effects. Its CPS translation generates λ-terms in which continuation composition is not expressed in terms of nested function calls, as is typical of other delimited-control operators, e.g. shift, but with function applications consuming a sequence of continuations one at a time, as if they formed a stack.