Formalizing Implementation Strategies for First-Class Continuations

Abstract. We present the first formalization of implementation straor 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 ass 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.

• Type: Conference
• Year: 2000
• Where: ESOP
• Authors: Olivier Danvy
• Keywords: Abstract Machine, ESOP 2000, First-class Continuations, Programming Languages, Straor First-class Continuations