Eager functions as processes

• We present a fully abstract encoding of the lambda-calculus in the pi-calculus. • We apply a recent technique of unique solution of equations to establish completeness of the encoding. • We revisit the original encoding of the call-by-value lambda-calculus due to Milner, show some shortcomings, and study two approaches to overcome these shortcomings. We study Milner's encoding of the call-by-value λ -calculus into the π -calculus. We show that, by tuning the encoding to two subcalculi of the π -calculus (Internal π and Asynchronous Local π ), the equivalence on λ -terms induced by the encoding coincides with Lassen's eager normal-form bisimilarity, extended to handle η -equality. As behavioural equivalence in the π -calculus we consider contextual equivalence and barbed congruence. We also extend the results to preorders. A crucial technical ingredient in the proofs is the recently-introduced technique of unique solutions of equations, further developed in this paper. In this respect, the paper also intends to be an extended case study on the applicability and expressiveness of the technique.