We study the operational semantics of an extension of Girard's System
$\Fomega$ with two control operators: an {\em abort} operation that abandons
the current control context, and a {\em callcc} operation that captures the
current control context.  Two classes of operational semantics are considered,
each with a call-by-value and a call-by-name variant, differing in their
treatment of polymorphic abstraction and instantiation.  Under the {\em
standard} semantics polymorphic abstractions are values and polymorphic
instantiation is a significant computation step; under the {\em ML-like}
semantics evaluation proceeds beneath polymorphic abstractions and polymorphic
instantiation is computationally insignificant.

Compositional, type-preserving continuation-passing style (cps) transformation
algorithms are given for the standard semantics, resulting in terms on which
all four evaluation strategies coincide.  This has as a corollary the
soundness and termination of well-typed programs under the standard evaluation
strategies.  In contrast, such results are obtained for the call-by- value
ML-like strategy only for a restricted sub-language in which constructor
abstractions are limited to values.  The ML-like call-by-name semantics is
indistinguishable from the standard call-by-name semantics when attention is
limited to complete programs.