A fully-abstract semantics of lambda-mu in the pi-calculus

Abstract

We study the lambda-mu-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 notions of weak equivalence for lambda-mu -- one based on weak reduction, two modelling weak head-reduction and weak explicit head reduction (all considering terms without weak head-normal form equivalent as well), and one based on weak approximation -- 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.

In Proceedings CL&C 2014, arXiv:1409.2593

References in corpus (1)

• From X to Pi; Representing the Classical Sequent Calculus in the Pi-calculus

Cited by in corpus (3)

• Characterisation of Approximation and (Head) Normalisation for $\lambda \mu$ using Strict Intersection Types
• Fully Abstract Encodings of $\lambda$-Calculus in HOcore through Abstract Machines
• A Strong Bisimulation for a Classical Term Calculus