A sound and complete axiomatization of delimited continuations

12 years 12 months ago
A sound and complete axiomatization of delimited continuations
The shift and reset operators, proposed by Danvy and Filinski, are powerful control primitives for capturing delimited continuations. Delimited continuation is a similar concept as the standard (unlimited) continuation, but it represents part of the rest of the computation, rather than the whole rest of computation. In the literature, the semantics of shift and reset has been given by a CPS-translation only. This paper gives a direct axiomatization of calculus with shift and reset, namely, we introduce a set of equations, and prove that it is sound and complete with respect to the CPS-translation. We also introduce a calculus with control operators which is as expressive as the calculus with shift and reset, has a sound and complete axiomatization, and is conservative over Sabry and Felleisen's theory for first-class continuations. Categories and Subject Descriptors D.3.1 [Programming Languages]: Formal Definitions and Theory; F.3.2 [Logics and Meanings of Programs]: Semantics of...
Yukiyoshi Kameyama, Masahito Hasegawa
Added 13 Dec 2009
Updated 13 Dec 2009
Type Conference
Year 2003
Where ICFP
Authors Yukiyoshi Kameyama, Masahito Hasegawa
Comments (0)