Abstract. This paper presents a type-preserving translation from the call-by-value λµ-calculus (λµv-calculus) [23] into a typed π-calculus, and shows it is fully abstract up to natural consistent contextual congruences in respective calculi. The full abstraction is proved via an inverse transformation from the typed π-terms which inhabit the λµv-types into the λµv-calculus [23] (the so-called definability argument), using proof techniques based on games semantics and process calculi.

While there are different notions of control which would be represented as distinct forms of typed interactions in the π-calculus, surprisingly the full-control, the λµ-calculus originally introduced by Parigot [24] and whose call-by-value version is later studied by Ong-Stewart [23], has a particularly simple representation as a subset of the linear π-calculus introduced in [31]. Since we already know quite a few properties about the linear π-calculus, for example the strong normalisability is instantly derived for the subcalculus for control from our result in [31]. A tight operational correspondence assisted by the definability result, as we have shown in this paper, would open a possibility to use typed π-calculi as a tool to investigate and analyse various control structures in a uniform setting, possibly integrated with other language primitives and operational structures.

In the rest of the extended abstract, we first introduce the linear π-calculus with control, present the embedding of the call-by-value λµ-calculus, then outlines the definability arguments. We then discuss how the definability leads to an equational full abstraction for suitably defined behavioural equivalence for the λµ-calculus. The extended abstract concludes with further topics and open issues on the connection between the calculi with control and the linear/affine typed π-calculi [2, 3, 11, 31].