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


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

[pdf file]

Back to Hassei's Research Page / Home Page