Formalizing Implementation Strategies for First-Class Continuations

Olivier Danvy


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.

Full Text:


This website uses cookies to allow us to see how the site is used. The cookies cannot identify you or any content at your own computer.

ISSN: 0909-0878 

Hosted by the Royal Danish Library and Aarhus University Library