An approach to call-by-name delimited continuations

Abstract

We show that a variant of Parigot's λ;μ-calculus, originally due to de Groote and proved to satisfy Böhm's theorem by Saurin, is canonically interpretable as a call-by-name calculus of delimited control. This observation is expressed using Ariola et al's call-by-value calculus of delimited control, an extension of λ;μ-calculus with delimited control known to be equationally equivalent to Danvy and Filinski's calculus with shift and reset. Our main result then is that de Groote and Saurin's variant of λ;μ-calculus is equivalent to a canonical call-by-name variant of Ariola et al's calculus. The rest of the paper is devoted to a comparative study of the call-by-name and call-by-value variants of Ariola et al's calculus, covering in particular the questions of simple typing, operational semantics, and continuation-passing-style semantics. Finally, we discuss the relevance of Ariola et al's calculus as a uniform framework for representing different calculi of delimited continuations, including "lazy" variants such as Sabry's shift and lazy reset calculus.