Authors: Herbelin, Hugo
Ghilezan, Silvia 
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
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 May 16, 2024

Page view(s)

checked on May 9, 2024

Google ScholarTM




Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.