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

• Main Authors: Steffen van Bakel, Maria Grazia Vigliotti
• Format: Article
• Language: English
• Published: Open Publishing Association 2014-09-01
• Series: Electronic Proceedings in Theoretical Computer Science
• Online Access: http://arxiv.org/pdf/1409.3314v1

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.