This paper presents a type-preserving translation from the call-by-value
-calculus ( v-calculus) into a typed -calculus, and shows full abstraction up to
maximally consistent observational congruences in both calculi. The -calculus
has a particularly simple representation as typed mobile processes where a unique
stateless replicated input is associated to each name. The corresponding -calculus
is a proper subset of the linear -calculus, the latter being able to embed the simplytyped
-calculus fully abstractly. Strong normalisability of the v-calculus is an
immediate consequence of this correspondence and the strong normalisability of the
linear -calculus, using the standard argument based on simulation between the
v-calculus and its translation. Full abstraction, our main result, is proved via an
inverse transformation from the typed -terms which inhabit the encoded v-types
into the v-calculus (the so-called de nability argument), using proof techniques
from games semantics and process calculi. A tight operational correspondence assisted
by the de nability result opens a possibility to use typed -calculi as a tool
to investigate and analyse behaviours of various control operators and associated
calculi in a uniform setting, possibly integrated with other language primitives and
operational structures.