Transformation of programs into continuation-passing style (CPS) reveals the
notion of continuations, enabling many applications such as control operators
and intermediate representations in compilers. Although type preservation makes
CPS transformation more beneficial, achieving type-preserving CPS transformation
for implicit polymorphism with call-by-value (CBV) semantics is known to be
challenging. We identify the difficulty in the problem that we call scope
intrusion. To address this problem, we propose a new CPS target language
$\Lambda^{open}$ that supports two additional constructs for
polymorphism: one only binds and the other only generalizes type variables.
Unfortunately, their unrestricted use makes $\Lambda^{open}$ unsafe due
to undesired generalization of type variables. We thus equip
$\Lambda^{open}$ with affine types to allow only the type-safe
generalization. We then define a CPS transformation from Curry-style CBV
System F to type-safe $\Lambda^{open}$ and prove that the transformation
is meaning and type preserving. We also study parametricity of
$\Lambda^{open}$ as it is a fundamental property of polymorphic languages
and plays a key role in applications of CPS transformation. To establish
parametricity, we construct a parametric, step-indexed Kripke logical relation
for $\Lambda^{open}$ and prove that it satisfies the Fundamental Property
as well as soundness with respect to contextual equivalence.