Formalizing Implementation Strategies for First-Class Continuations
Olivier Danvy December 1999 |
Abstract:
We present the first formalization of implementation strategies for
first-class continuations. The formalization hinges on abstract
machines for continuation-passing style (CPS) programs with a
special treatment for the current continuation, accounting for the
essence of first-class continuations. These abstract machines are
proven equivalent to a standard, substitution-based abstract
machine. The proof techniques work uniformly for various
representations of continuations. As a byproduct, we also present a
formal proof of the two folklore theorems that one continuation
identifier is enough for second-class continuations and that
second-class continuations are stackable.
A large body of work exists on implementing continuations, but it is predominantly empirical and implementation-oriented. In contrast, our formalization abstracts the essence of first-class continuations and provides a uniform setting for specifying and formalizing their representation.
Available as PostScript, PDF, DVI. |