Typing First-Class Continuations in ML

Abstract

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.