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. |

Published: 9th September 2014.

ArXived at: http://dx.doi.org/10.4204/EPTCS.164.3 | bibtex | |

Comments and questions to: eptcs@eptcs.org |

For website issues: webmaster@eptcs.org |