|Title:||An approach to call-by-name delimited continuations||Journal:||ACM SIGPLAN Notices||Volume:||43||Issue:||1||First page:||383||Last page:||394||Issue Date:||1-Jan-2008||Rank:||M23||ISSN:||0362-1340||DOI:||10.1145/1328897.1328484||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.
|Keywords:||Böhm separability | Classical logic | Delimited control | Observational completeness||Publisher:||Association for Computing Machinery|
Show full item record
checked on Mar 20, 2023
checked on Mar 21, 2023
Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.