Typing First-Class Continuations in ML

An extension of Standard ML with continuation primitives similar to those found in Scheme is considered. A number of alternative type systems are discussed, and several programming examples are given. The semantics of type assignment for a small, purely functional fragment of the language is presented, for which both a Milner-style soundness theorem and an observational soundness theorem may be established. 1 Introduction First-class continuations are a simple and natural way to provide access to the flow of evaluation in functional languages. The ability to seize the "current continuation " (control state of the evaluator) provides a simple and natural basis for defining numerous higherlevel constructs such as coroutines [15], exceptions [41], and engines [6], for writing interpreters and compilers [30, 34], and for organizing run-time support for multiple threads of control [40, 27]. Tractable logics for reasoning about program equivalence in the presence of first-class continuation..