We study the operational semantics of an extension of Girard's System
F-omega with two control operators: an <I>abort</I> operation that
abandons the current control context, and a <I>callcc</I> 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 <I>standard</I> semantics polymorphic
abstractions are values and polymorphic instantiation is a significant
computation step; under the <I>ML-like</I> 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.