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 higher-level
constructs such as coroutines~\cite{haynes+86},
exceptions~\cite{wright+90}, and logic
variables~\cite{felleisen85,haynes87}, for supporting multiple threads
of control~\cite{wand80,haynes+87b,reppy89,dybvig+89}, for providing
asynchronous signal handlers~\cite{reppy90}, and for implementing
non-blind backtracking~\cite{friedman+85} and dynamic barriers such as
unwind-protect~\cite{haynes+87a}.  Tractable logics for reasoning
about program equivalence in the presence of first-class continuations
in an untyped setting have been
developed~\cite{felleisen+86b,felleisen+87,talcott88}. Recent studies
of continuations have addressed the question of their typing in a
restricted setting~\cite{filinski89a,filinski89b,griffin90} and their
impact on full abstraction results~\cite{sitaram+90}.

The subject of this paper is the extension of Standard ML with
primitives for first-class continuations similar to those found in
Scheme.  The two new primitives are {\tt callcc}, for {\em call with
current continuation}, which takes a function as argument and calls
it with the current continuation, and {\tt throw}, which takes a
continuation and a value and passes the value to that continuation.
%In contrast to Scheme, continuations are not regarded as ordinary
%functions, but rather are treated as values of type {\tt 'a cont}, the
%type of continuations accepting values of type {\tt 'a}.  On the other
%hand, the SML {\tt callcc} primitive is similar to that found in
%Scheme in that the called function need not necessarily invoke the
%continuation, but may instead return a value to the evaluation
%context.  Thus the type of {\tt callcc} is {\tt ('a cont -> 'a) ->
%'a}, reflecting the operational behavior just described.  Since
%continuations are not functions, a primitive for passing values to a
%continuation is needed.  This primitive is called {\tt throw}; it
%takes a continuation and a value, and invokes the continuation on that
%value.  Since continuations never return to the point of the call, the
%result type of a {\tt throw} invocation is arbitrary (\cf{} {\tt
%raise} in SML).  Thus the type of {\tt throw} is {\tt 'a cont -> 'a ->
%'b}.

This paper is organized as follows.  In Section~\ref{adding-sec} we give an
informal presentation of the extension of ML with continuation primitives, and
illustrate their use in programming examples.  We also discuss the role of
continuations in the implementation of Standard ML of New Jersey, and some
problems that they raised.  In Section~\ref{pta-sec} we present a formal
system of type assignment for a small functional fragment of ML.  A
denotational semantics for this fragment is given in Section~\ref{pta-sec},
and the semantics of type assignment is considered.

We are grateful to Andrew Appel, Stephen Brookes, Matthias Felleisen,
Andrzej Filinski, Timothy Griffin, John Reppy, Didier R\'{e}my, Olin
Shivers, and Mads Tofte for their comments and suggestions.
