A sound and complete axiomatization of delimited continuations
Yukiyoshi Kameyama and Masahito Hasegawa
In Proc.
8th ACM SIGPLAN International Conference on Functional Programming (ICFP 2003)
pages 177-188
Abstract
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.
keywords: continuation, CPS-translation, axiomatization.
© ACM 2003
Back to Hassei's
Research Page / Home Page