In this section we make precise the informal ideas presented in
Section~\ref{adding-sec}.  We begin by recalling the polymorphic type
assignment system introduced by Damas and Milner~\cite{damas+82}.  This type
system will form the basis of our investigation of the typing properties of
the continuation-passing primitives introduced in Section~\ref{adding-sec}.
We then give a continuation-passing structured operational semantics for this
language, and prove the soundness of type assignment with respect to this
semantics.  (This answers a question posed by Robin Milner [private
communication].) We then show that the extension of the Damas-Milner type
system with the continuation-passing primitives of Section~\ref{adding-sec} is
unsound.\footnote{This result was jointly obtained by the first author and
Mark Lillibridge in the summer of 1991.}  We consider two approaches to
recovering soundness, one based on the restriction of polymorphism to values,
and the other based on Tofte's notion of imperative type
variable~\cite{tofte90}.

\subsection{The Damas-Milner Language}

We begin by recalling the polymorphic type assignment system introduced by
Damas and Milner~\cite{damas+82}.

The syntax of {\em ordinary expressions} is given by the following grammar:
\[
\begin{array}{lrcl}
{\it expressions} & e	& \GoesTo	&
x \Or c \Or \lambda x.e \Or e_1\,e_2 \Or \Letbe{x}{e_1}{e_2}
\end{array}
\]
The metavariable $x$ ranges over a countably infinite set of variables, and
the metavariable $c$ ranges over a countable set of constants.  The set
$\FV(e)$ of variables occuring freely in $e$ is defined as usual, as is the
operation of capture-avoiding substitution of an expression $e$ for free
occurrences of a variable $x$ in another expression $e'$, written $[e/x]e'$.

The syntax of {\em type expressions} is given by the following grammar:
\[
\begin{array}{lrcl}
{\it monotypes} & \tau		& \GoesTo	&
b \Or t \Or \tau_1{\to}\tau_2 \\
{\it polytypes} & \sigma	& \GoesTo	&
\tau \Or \forall t.\sigma
\end{array}
\]
The metavariable $t$ ranges over a countably infinite set of {\em type
variables}, and the metavariable $b$ ranges over a countable set of {\em base
types}.  The set $\FTV(\sigma)$ of type variables occurring freely in a
polytype $\sigma$ is defined as usual, as is the operation of capture-avoiding
substitution of a monotype $\tau$ for free occurrences of a type variable $t$
in a poltype $\sigma$, written $[\tau/t]\sigma$.

A {\em context} is a finite sequence of variable declarations of the form
$x{:}\sigma$ assigning the polytype $\sigma$ to the variable $x$, subject to
the condition that no variable may be assigned more than one polytype.  The
variable $\Gamma$ ranges over contexts.  The ``no redeclaration'' condition
implies that a context may be regarded as a partial function sending a
variable $x$ to the unique (if it exists) $\sigma$ such that $x{:}\sigma$ is
in $\Gamma$.  We write $\Dmn(\Gamma)$ for the domain of $\Gamma$ regarded
as a partial function, and $\Gamma,x{:}\sigma$, where $x\not\in\Dmn(\Gamma)$,
for the extension of $\Gamma$ with the given declaration.  The set of type
variables occuring freely in a context $\Gamma$, written $\FTV(\Gamma)$, is
defined to be $\bigcup_{x\in\Dmn(\Gamma)}\FTV(\Gamma(x))$.  A {\em signature}
is a finite sequence of constant declarations of the form $c{:}\sigma$,
subject to the condition that no constant is declared more than once.
Notational conventions similar to those for contexts apply to signatures.

We shall work with a syntax-directed formulation of the Damas-Milner
polymorphic type assignment system inspired by the static semantics of
Standard ML~\cite{milner+90}.  The rules given in Table~\ref{dm-table} define
a formal system for deriving judgements of the form $\Gamma\ts e:\tau$,
expressing that the expression $e$ may be assigned the monotype $\tau$ in
context $\Gamma$.  The rules are parametric in a signature $\Sigma$, which we
leave implicit.  We often write $\Gamma\ts e:\tau$, or just $e:\tau$ when
$\Gamma$ is empty, to mean that this typing judgement is derivable in
accordance with the rules of Table~\ref{dm-table}.  An expression $e$ is said
to be {\em well-typed} in a context $\Gamma$ iff there exists a $\tau$ such
that $\Gamma\ts e:\tau$.

Some of the rules given in Table~\ref{dm-table} make use of auxiliary notions
that merit further explanation.  Rule~\ruleref{var} makes use of the {\em
polymorphic instance} relation $\sigma\geq\tau$ which is defined to hold iff
$\sigma$ is a polytype of the form $\forall t_1.\ldots.\forall t_n.\tau'$ and
$\tau$ is a monotype of the form $[\tau_1,\ldots,\tau_n/t_1,\ldots,t_n]\tau'$
for some monotypes $\tau_1$, \ldots, $\tau_n$.  This relation is extended to
polytypes by defining $\sigma\geq\sigma'$ iff $\sigma\geq\tau$ whenever
$\sigma'\geq\tau$.  Rule~\ruleref{let} makes use of {\em polymorphic
generalization} of a monotype $\tau$ in a context $\Gamma$,
$\Close_\Gamma(\tau)$, defined to be the polytype $\forall t_1.\ldots.\forall
t_n.\tau$, where $\FTV(\tau)\setminus\FTV(\Gamma)=\{\,t_1,\ldots,t_n\,\}$.  We
sometimes abbreviate $\Close_\Gamma(\tau)$ to just $\Close(\tau)$ when
$\Gamma$ is the empty context.

The formal system of Table~\ref{dm-table} is clearly a subsystem of the system
given by Damas and Milner~\cite{damas+82} in the sense that if $\Gamma\ts
e:\tau$ is derivable in the system of Table~\ref{dm-table}, then it is
derivable in Damas and Milner's system.  Conversely, if $\Gamma\ts e:\sigma$
is derivable in Damas and Milner's system, then $\Gamma\ts e:\tau$ is
derivable in the system of Table~\ref{dm-table} whenever $\sigma\geq\tau$.
Thus all and only the monotypes derivable for a given term in Damas and
Milner's system are derivable in the system considered here.  The advantage of
the formulation given here is that the rules are syntax-directed in that there
is precisely one rule for each form of ordinary expression.

The key to ML-style polymorphic type checking is the existence of a ``most
general'' type for an expression in a given context.\cite{damas+82}
\begin{thm}[Damas and Milner]
If the expression $e$ is typable in context $\Gamma$, then there exists a {\em
principal type} $\tau$ for $e$ in $\Gamma$ with the property that $\Gamma\ts
e:\tau$, and for every $\tau'$ such that $\Gamma\ts e:\tau'$,
$\Close_\Gamma(\tau)\geq\tau'$.
\end{thm}

The following lemma summarizes some important properties of the type system.
\begin{lemma}
\label{dm-tech-lemma}
\begin{enumerate}
\item If $\Gamma\ts e:\tau$ and $x\in\FV(e)$, then $x\in\Dmn(\Gamma)$.
\item If $\Gamma\ts e:\tau$, $x\not\in\Dmn(\Gamma)$, and
$\FTV(\sigma)\subseteq\FTV(\Gamma)$, then $\Gamma,x{:}\sigma\ts e:\tau$.
\item If $\Gamma\ts e:\tau$ and $\Gamma,x{:}\sigma\ts e':\tau'$ with
$\Close_\Gamma(\tau)\geq\sigma$, then $\Gamma\ts [e/x]e':\tau'$.
\end{enumerate}
\end{lemma}

\begin{table}
\begin{inferencerule}{var}
\infrule{\Gamma(x)\geq\tau}{\Gamma\ts x:\tau}{}
\end{inferencerule}
\begin{inferencerule}{const}
\infrule{\Sigma(c)\geq\tau}{\Gamma\ts c:\tau}{}
\end{inferencerule}
\begin{inferencerule}{abs}
\infrule{\Gamma,x{:}\tau_1\ts e:\tau_2}{\Gamma\ts\lambda x.e : \tau_1{\to}\tau_2}{(x\not\in\Dmn(\Gamma))}
\end{inferencerule}
\begin{inferencerule}{app}
\infrule{\Gamma\ts e_1:\tau_2{\to}\tau \qquad \Gamma\ts e_2:\tau_2}{\Gamma\ts
e_1\,e_2 : \tau}{}
\end{inferencerule}
\begin{inferencerule}{let}
\infrule{\Gamma\ts e_1:\tau_1 \qquad \Gamma,x{:}\Close_\Gamma(\tau_1)\ts e_2:\tau_2}{\Gamma\ts\Letbe{x}{e_1}{e_2}:\tau_2}{(x\not\in\Dmn(\Gamma))}
\end{inferencerule}
\caption{Polymorphic Type Assignment}
\label{dm-table}
\end{table}

\subsection{Operational Semantics}

The operational semantics of untyped terms is a three-place relation $k\ts
e\Rightarrow a$ defined by a set of syntax-directed inference rules.  Here $e$
is the expression being evaluated, $k$ is a ``continuation'' representing the
current evaluation context, and $a$ is the final ``answer'' obtained by
evaluating $e$ in context $k$.

The semantics is defined in terms of three additional syntactic categories,
defined by the following grammar:
\[
\begin{array}{lrcl}
{\it values}	& v	& \GoesTo	& c \Or \lambda x.e \\
{\it continuations} & k	& \GoesTo	& \Hole \Or k\,e \Or v\,k \Or \Letbe{x}{k}{e} \\
{\it answers}	& a	& \GoesTo	& v \Or \Wrong
\end{array}
\]
Values, continuations, and answers are all assumed to have no free variables.
A continuation $k$ has precisely one ``hole'', designated by the symbol
``$\Hole$''.  If $k$ is a continuation, we write $k[e]$ for the
expression obtained by ``filling'' the hole in $k$ with the expression $e$.
Similarly, if $k'$ is another continuation, $k[k']$ is the
continuation that results from filling the hole in $k$ with $k$'.

The operational semantics of the language of untyped terms given above is
defined by the rules of Table~\ref{op-sem-table}.  We sometimes write
$e\Rightarrow a$ to mean $\Hole\ts e\Rightarrow a$.

\begin{table}
\begin{inferencerule}{val0}
\axiom{\Hole\ts v\Rightarrow v}{}
\end{inferencerule}
\begin{inferencerule}{val1}
\infrule{\Hole\ts k[v]\Rightarrow a}{k\ts v\Rightarrow a}{(k\not=\Hole)}
\end{inferencerule}
\begin{inferencerule}{fn}
\infrule{k[\Hole\,e_2]\ts e_1\Rightarrow a}{k\ts e_1\,e_2\Rightarrow a}{}
\end{inferencerule}
\begin{inferencerule}{arg}
\infrule{k[v_1\,\Hole]\ts e_2\Rightarrow a}{k\ts v_1\,e_2\Rightarrow a}{}
\end{inferencerule}
\begin{inferencerule}{beta}
\infrule{k\ts [v_2/x]e_1\Rightarrow a}{k\ts (\lambda x.e_1)\,v_2\Rightarrow a}{}
\end{inferencerule}
\begin{inferencerule}{wrong}
\axiom{k\ts v_1\,v_2\Rightarrow\Wrong}{(v_1\not=\lambda x.e)}
\end{inferencerule}
\begin{inferencerule}{bind}
\infrule{k[\Letbe{x}{\Hole}{e_2}]\ts e_1\Rightarrow
a}{k\ts\Letbe{x}{e_1}{e_2}\Rightarrow a}{}
\end{inferencerule}
\begin{inferencerule}{sub}
\infrule{k\ts[v_1/x]e_2\Rightarrow a}{k\ts\Letbe{x}{v_1}{e_2}\Rightarrow a}{}
\end{inferencerule}
\caption{Operational Semantics}
\label{op-sem-table}
\end{table}

The idea underlying the operational semantics is that in a judgement $k\ts
e\Rightarrow a$ the continuation $k$ represents an ``evaluation context'' (in
the sense of Felleisen~\cite{felleisen}), and $e$ represents the expression
being evaluated in that context.  If $e$ is a value, then evaluation continues
by replacing the ``hole'' in $k$ with $v$, and re-starting the evaluation
process.  If $e$ is not a value, then either it is reducible by
rule~\ruleref{beta} or~\ruleref{sub}, in which case the reduction is
performed, or else evaluation proceeds to a sub-expression of $e$, extending
the continuation $k$ accordingly.

\subsection{Soundness of Type Assignment}

The soundness of the polymorphic type system with respect to the operational
semantics is summarized by the slogan ``well-typed programs cannot go wrong''.
In other words, if a program has a type according to the type assignment
system, then evaluation of that program, starting in the empty context, cannot
result in the answer $\Wrong$.  We prove a slightly stronger result admitting
general evaluation contexts, and phrase the theorem in terms of preservation
of typing under evaluation.  (See Felleisen and Wright~\cite{wright+91} for
a similar perspective.)

\begin{thm}
\label{dm-soundness-thm}
Let $\alpha$ be an arbitrary monotype.  If $k\ts e\Rightarrow a$ with $e:\tau$
and $x{:}\Close(\tau)\ts k[x]:\alpha$, then $a$ is a value and $a:\alpha$.
\end{thm}
{\bf Proof}\ The proof proceeds by induction on the structure of the
derivation of $k\ts e\Rightarrow a$.
\begin{description}
\item[\ruleref{val0}:] In this case $e=v=a$ and $k = \Hole$.  It is
immediate that $a$ is a value.  We assume
$v:\tau$ and $x{:}\Close(\tau)\ts x : \alpha$ since $k[x] = x$, and it
follows from Lemma~\ref{dm-tech-lemma}, part 3 that $v{:}\alpha$, and
hence $a{:}\alpha$.
\item[\ruleref{val1}:] Assuming $k\not=\Hole$ we have by rule
\ruleref{val1} that $\Hole\ts k[v]\Rightarrow a$.  From the
assumptions that $v:\tau$ and $x{:}\Close(\tau)\ts k[x] : \alpha$ and
Lemma~\ref{dm-tech-lemma}, part 3, it follows that $k[v]:\alpha$.
Clearly $x{:}\Close(\alpha)\ts x{:}\alpha$, and hence $a:\alpha$ by induction.
\item[\ruleref{fn}:] By rule \ruleref{fn} we have
$k[\Hole\,e_2]\ts e_1\Rightarrow a$.  By type rule \ruleref{app} we
have $e_1 : \tau_2{\to}\tau$ and $e_2 : \tau_2$ for some type $\tau_2$.
By Lemma~\ref{dm-tech-lemma}, part 2, and the type assumption on $k$ we have 
$y{:}\Close(\tau_2{\to}\tau),x{:}\Close(\tau)\ts k[x] : \alpha$, and
clearly $y{:}\Close(\tau_2{\to}\tau)\ts y\,e_2 : \tau$.  Hence by
Lemma~\ref{dm-tech-lemma}, part 3, we have
$y{:}\Close(\tau_2{\to}\tau)\ts k[[y]e2] : \alpha$.  It follows by
induction that $a : \alpha$.
% It suffices to show that $x{:}\Close(\tau_2{\to}\tau)\ts
% x\,e_2 : \tau$, for then by Lemma~\ref{dm-tech-lemma} and the assumptions,
% $x{:}\Close(\tau_2{\to}\tau)\ts k[x\,e_2]:\alpha$.  But this follows from the
% inductive assumptions, with an application of Lemma~\ref{dm-tech-lemma}.
\item[\ruleref{arg}:] Since $v_1\,e_2 : \tau$ there is a type $\tau_2$
such that $v_1 : \tau_2{\to}\tau$ and $e_2 : \tau_2$.  It suffices to
show that $y{:}\Close(\tau_2)\ts k[v_1\,y] : \alpha$, which follows
from $y{:}\Close(\tau_2)\ts v_1\,y : \tau$ by an argument similar to that of 
the \ruleref{fn} case.
% It suffices to show that
% $x{:}\Close(\tau)\ts v_1\,x : \tau$, which follows from the inductive
% assumptions by an application of Lemma~\ref{dm-tech-lemma}.
\item[\ruleref{beta}:] We have $k\ts [v_2/x]e_1\Rightarrow a$ by the
\ruleref{beta} rule, and $x{:}\Close(\tau)\ts k[x] : \alpha$ by assumption.
It suffices to show that $[v_2/x]e_1:\tau$.  This follows from the
assumption that $(\lambda x.e_1)\,v_2 : \tau$ by the typing rules and
an application of Lemma~\ref{dm-tech-lemma}, part 3.
\item[\ruleref{wrong}:] By assumption $v_1\,v_2:\tau$, and hence
$v_1:\tau_2\to\tau$ for some monotype $\tau_2$.  Since the value $v_1$
is assumed not to be a $\lambda$-abstraction, it must be a constant.
But there are no constants of functional type, yielding a contradiction.
Therefore this rule will not apply to a well-typed expression.
\item[\ruleref{bind}:] By the \ruleref{let} typing rule, there exists
a type $\tau_1$ such that $e_1 : \tau_1$ and $x{:}\Close(\tau_1)\ts
e_2 : \tau$.  From the typing rules we can show that $y:\Close(\tau_1)\ts
\Letbe{x}{y}{e_2} : \tau$, and using Lemma~\ref{dm-tech-lemma} as
before we obtain $y{:}\Close(\tau_1)\ts k[\Letbe{x}{y}{e_2}] : \alpha$.
We can then conclude that $a : \alpha$ by the induction hypothesis.
\item[\ruleref{sub}:] This case is similar to the \ruleref{beta} case.
It suffices to show that $[v_1/x]e_2:\tau$, which follows
from the inductive assumptions by an application of
Lemma~\ref{dm-tech-lemma}, part 3.
\qed
\end{description}

The soundness of the polymorphic type system with respect to the continuation
semantics follows directly:
\begin{cor}
If $e$ is a well-typed program of type $\tau$, and $e\Rightarrow a$, then
$a\not=\Wrong$.
\end{cor}
{\bf Proof}\ Take $\alpha=\tau$ and $k=\Hole$ in
Theorem~\ref{dm-soundness-thm}.\qed

\subsection{First-Class Continuations}

To account for the continuation-passing primitives introduced in
Section~\ref{adding-sec}, we extend the language of monotypes as follows:
\[
\begin{array}{lrcl}
{\it monotypes}	& \tau	& \GoesTo	& \ldots \Or \tau\,\Cont
\end{array}
\]
The signature $\Sigma_{\Cont}$ is given by the following declarations:
\[
\begin{array}{rcl}
\CallccSymbol	& :	& \forall t.(t\,\Cont{\to} t){\to} t \\
\ThrowSymbol	& :	& \forall s.\forall t.s\,\Cont{\to}s{\to}t
\end{array}
\]

The operational semantics of $\CallccSymbol$ and $\Throw$ is defined in such a
way that continuations must be ``reified'' as values.  Accordingly we extend
the syntax of values:
\[
\begin{array}{lrcl}
{\it values}	& v	& \GoesTo	& \ldots \Or k
\end{array}
\]
The typing relation $v:\tau$ is extended to this additional case by defining
$k:\tau\,\Cont$ to hold iff $x{:}\tau\ts k[x]:\alpha$, where $\alpha$ is a
fixed type of answers.

The extension of the operational semantics to cover $\CallccSymbol$ and
$\ThrowSymbol$ is given in Table~\ref{callcc-table}.
\begin{table}
\begin{inferencerule}{seize}
\infrule{k\ts v\,k\Rightarrow a}{k\ts \CallccSymbol\,v\Rightarrow a}{}
\end{inferencerule}
\begin{inferencerule}{jump}
\infrule{k'\ts v\Rightarrow a}{k\ts \ThrowSymbol\,k'\,v\Rightarrow a}{}
\end{inferencerule}
\begin{inferencerule}{wrong}
\axiom{k\ts v_1\,v_2\Rightarrow\Wrong}{(v_1\not=\lambda x.e,\ v_1\not\in\{\,\CallccSymbol,\ThrowSymbol\,\})}
\end{inferencerule}
\caption{Semantics of Continuation-Passing Primitives}
\label{callcc-table}
\end{table}

We turn now to the question of soundness of type assignment for the extension
of the semantics with first-class continuations.  Despite the superficial
plausibility of the typing rules for $\CallccSymbol$ and $\ThrowSymbol$, the
full polymorphic type assignment system for the extended language is
unsound.~\footnote{This result was obtained jointly by Mark Lillibridge and
the first author.} Specifically, assume that we have base types $\Int$ and
$\Bool$, and constants $\True:\Bool$ and $1:\Int$.  The following program has
type ${\it bool}$ in the empty context, but yields answer $1$ when evaluated
in the empty context:
\[
\Letbe{f}{\CallccSymbol\,(\lambda k.\lambda x.\ThrowSymbol\,k\,(\lambda
y.x))}{f\,1\ ;\ f\,\True}
\]
To see what is wrong, it is helpful to consider a na\"\i{}ve attempt to extend
the proof of Theorem~\ref{dm-soundness-thm} to the present setting.
Difficulties arise only in the case of~\ruleref{seize}.  Specifically, we have
by assumption that $k\ts \Callcc\,v\Rightarrow a$ with $\Callcc\,v : \tau$ and
$x{:}\Close(\tau)\ts k[x] : \alpha$.  We are to show that $a:\alpha$.  For the
induction it suffices to show that $v\,k : \tau$, for which it is sufficient
to show that $v:\tau\,\Cont\to\tau$ and that $k:\tau\,\Cont$, which is to say
$x{:}\tau\ts k[x]:\alpha$.  But all we have is the weaker condition
$x{:}\Close(\tau)\ts k[x]:\alpha$, which is not sufficient.  The
counterexample shows that this failure is essential: the soundness theorem is
false for the enriched language.

The essential difficulty is that a continuation of the form
$k[\Letbe{x}{\Hole}{e}]$ may use its argument polymorphically, but this
requirement is not expressible in the Damas-Milner type discipline.  Such
continuations arise because of the sequential evaluation of $\LetSymbol$
expressions in a call-by-value language.  However, if we restrict the language
so that $\LetSymbol$-bound expressions are required to be values, then the
rule~\ruleref{bind} may be dropped from the operational semantics, and there is
no need for continuations of the above form.  As a consequence
Theorem~\ref{dm-soundness-thm} may be strengthened by relaxing the condition
on $k$ to $x{:}\tau\ts k[x]:\alpha$.  We may then extend the theorem to
$\CallccSymbol$ and $\ThrowSymbol$, as follows.
\begin{thm}
Suppose that $\LetSymbol$ expressions are limited to bind only values.
If $k\ts e\Rightarrow a$ with $e:\tau$ and $x{:}\tau\ts k[x]:\alpha$, then
$a:\alpha$.
\end{thm}
{\bf Proof}\ Similar to the proof of Theorem~\ref{dm-soundness-thm}, amended
as follows:
\begin{description}
\item[\ruleref{seize}:]
By assumption $\CallccSymbol\,v:\tau$, and hence $v:\tau\,\Cont\to\tau$.  It
suffices to show that $v\,k:\tau$, which follows from $k:\tau\,\Cont$, which
follows from $x{:}\tau\ts k[x]:\alpha$, which holds by assumption.
\item[\ruleref{jump}:]
By the inductive assumptions $\ThrowSymbol\,v\,k:\tau$, which implies that
$v:\tau$ and $k:\tau\,\Cont$, and consequently that $x{:}\tau\ts k[x]:\alpha$.
The result then follows by an application of the inductive hypothesis.
\item[\ruleref{wrong}:]
If $v_1$ is neither a $\lambda$-abstraction nor $\CallccSymbol$ nor
$\ThrowSymbol$, then it cannot be well-typed.
\end{description}
Note that the~\ruleref{bind} case no longer arises due to the restrictions on
$\LetSymbol$ expressions.\qed
\noindent

The restriction of polymorphic $\LetSymbol$ expressions to binding only values
is a rather drastic departure from the pure polymorphic core language.  In
fact we need only ensure that whenever a $\CallccSymbol\,v$ is evaluated, then
the context of evaluation must type check monomorphically.  By requiring
$\LetSymbol$-bound expressions to be values, we ensure that no polymorphic
continuations ever arise, but this seems draconian.  In particular, there are
sound programs that violate this condition.\footnote{Example?} A more flexible
approach based on Tofte's notion of {\em imperative type
variables}~\cite{tofte90} leads to a more flexible language, at the expense of
complicating the type system somewhat.

The main idea is to distinguish a countably infinite subset of type variables,
called {\em critical} type variables.  In the syntax for type expressions
critical type variables are marked with an underscore ($\underline{\:}$).  The
universal quantifier may bind both ordinary and critical type variables, but
we restrict polymorphic instantiation and generalization as follows.  First,
generalization is re-defined so that only ordinary type variables are
quantified.  Specifically, $\Close_\Gamma(\tau) = \forall t_1.\ldots.\forall
t_n.\tau$, where $\FTV(\tau)\setminus\FTV(\Gamma) =
\{\,t_1,\ldots,t_n,\underline{t_1'},\ldots,\underline{t_m'}\,\}$.
A monotype is called {\em critical} iff all of its type variables are
critical.  Polymorphic instantiation is re-defined so that a critical type
variable may only be instantiated by a critical type.  Thus in particular
$\forall\underline{t}.\underline{t}{\to}\underline{t}\geq
(\underline{t}{\to}\underline{t}){\to}(\underline{t}{\to}\underline{t})$, but
$\forall\underline{t}.\underline{t}{\to}\underline{t}\not\geq
(t{\to}t){\to}(t{\to}t)$

We apply the technology of critical type variables by defining
the signature $\Sigma'_{\Cont}$ as follows:
\[
\begin{array}{rcl}
\CallccSymbol	& :	& \forall \underline{t}.(\underline{t}\,\Cont{\to} \underline{t}){\to} \underline{t} \\
\ThrowSymbol	& :	& \forall s.\forall t.s\,\Cont{\to}s{\to} t
\end{array}
\]
Notice that only the type of $\CallccSymbol$ is changed compared to
$\Sigma_{\Cont}$.  Using this signature we may extend
Theorem~\ref{dm-soundness-thm} to admit first-class continuations without
modifying the typing rule for $\LetSymbol$ expressions (beyond the
re-definition of $\Close$, that is).  For if $\Callcc\,v:\tau$, then $\tau$
must be a critical monotype, and hence $\Close(\tau)=\tau$.  But then the
assumption $x{:}\Close(\tau)\ts k[x]:\alpha$ is equivalent to the weaker
condition $x{:}\tau\ts k[x]:\alpha$ required for $k:\tau\,\Cont$ to hold,
which is sufficient for the inductive hypothesis to apply, as disccused above.
Consequently, the use of critical type variables suffices for the soundness of
first-class continuation primitives in a polymorphic language.

Finally, as noted by Tofte~\cite{tofte90}, it is possible to combine the two
approaches to recovering soundness so as to admit more programs than either
approach alone.  In particular, it is sound to fully generalize the type of a
$\LetSymbol$-bound expression provided that it is a value, and provided that
the distinction between critical and ordinary type variables is preserved.
The resulting system is sound (by a combination of the proofs of the soundness
of each approach separately), and admits more programs than either
alone.~\footnote{Examples?}


