Control in the Pi-Calculus (with Nobuko Yoshida and Kohei Honda)

This paper presents a type-preserving translation from the call-by-value lambda mu-calculus (lambda mu v-calculus) into a typed pi-calculus, and shows full abstraction up to maximally consistent observational congruences in both calculi. The lambda mu-calculus has a particularly simple representation as typed mobile processes where a unique stateless replicated input is associated to each name. The corresponding pi-calculus is a proper subset of the linear pi-calculus, the latter being able to embed the simply-typed lambda-calculus fully abstractly. Strong normalisability of the lambda mu v-calculus is an immediate consequence of this correspondence and the strong normalisability of the linear pi-calculus, using the standard argument based on simulation between the lambda mu v-calculus and its translation. Full abstraction, our main result, is proved via an inverse transformation from the typed pi-terms which inhabit the encoded lambda mu v-types into the lambda mu v-calculus (the so-called definability argument), using proof techniques from games semantics and process calculi. A tight operational correspondence assisted by the definability result opens a possibility to use typed pi-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.

Extended abstract: ps.gz, pdf, Bibtex.
Full version: ps.gz, pdf, Status: submitted.

$Id: index.html,v 1.7 2006/02/09 19:28:57 martinb Exp $