A fully-abstract semantics of λμ in the π-calculus

Abstract

We study the λμ-calculus, extended with explicit substitution, and define a compositional outputbased interpretation into a variant of the π-calculus with pairing that preserves single-step explicit head reduction with respect to weak bisimilarity. We define four notions of weak equivalence for λμ-one based on weak reduction ∼<inf>wβμ</inf>, two modelling weak head-reduction and weak explicit head reduction, ∼<inf>wH</inf> and ∼<inf>wxH</inf> respectively (all considering terms without weak head-normal form equivalent as well), and one based on weak approximation ∼A-and show they all coincide. We will then show full abstraction results for our interpretation for the weak equivalences with respect to weak bisimilarity on processes.