Lambda-calculus, multiplicities and the pi-calculus, with C. Laneve, INRIA Research Report 2581 (June 1995).

Abstract: (see also RR-2581)
In this paper we study the semantics of the lambda-calculus induced by Milner's encoding into the pi-calculus. We show that the resulting may testing preorder on lambda-terms coincides with the inclusion of Lévy-Longo trees. To establish this result, we use a refinement of the lambda-calculus where the argument of a function may be of limited availability. In our lambda-calculus with multiplicities, evaluation is deterministic, but it may deadlock, due to the lack of resources. We show that this feature is enough to make the lambda-calculus as discriminating as the pi-calculus.

[Report, .ps.gz]