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

Steffen van Bakel
(Imperial College London)
Maria Grazia Vigliotti
(Adelard PLC)

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 Paulo Oliva: Proceedings Fifth International Workshop on Classical Logic and Computation (CL&C 2014), Vienna, Austria, July 13, 2014, Electronic Proceedings in Theoretical Computer Science 164, pp. 33–47.
Published: 9th September 2014.

ArXived at: https://dx.doi.org/10.4204/EPTCS.164.3 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org