A fully-abstract semantics of λµ in the pi-calculus (To appear in EPTCS)

We study the λµ-calculus, extended with explicit substitution, and define a compositional output-based interpretation into a variant of the pi-calculus with pairing that preserves single-step explicit head reduction with respect to weak bisimilarity. We define four no-tions of weak equivalence for λµ – one based on weak reduction ∼wβµ, two modelling weak head-reduction and weak explicit head reduction, ∼wh and ∼wxh respectively (all consid-ering 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 re-sults for our interpretation for the weak equivalences with respect to weak bisimilarity on processes