Typing First-Class Continuations in ML

An extension of 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. Acontinuation-based operational semantics is defined for a small, purely functional, language, and thesoundness of the Damas-Milner polymorphic type assignment system with respect to this semanticsis proved. The full Damas-Milner type system is shown to be unsound in the presence of first-class...