A fully-abstract semantics of λμ in the π-calculus
File(s)1409.3314v1.pdf (209.01 KB)
Published version
Author(s)
Van Bakel, S
Vigliotti, MG
Type
Conference Paper
Abstract
We study the λμ-calculus, extended with explicit substitution, and define a compositional outputbased interpretation into a variant of the π-calculus with pairing that preserves single-step explicit head reduction with respect to weak bisimilarity. We define four notions of weak equivalence for λμ-one based on weak reduction ∼<inf>wβμ</inf>, two modelling weak head-reduction and weak explicit head reduction, ∼<inf>wH</inf> and ∼<inf>wxH</inf> respectively (all considering 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 results for our interpretation for the weak equivalences with respect to weak bisimilarity on processes.
Date Issued
2014-09-11
Date Acceptance
2014-09-11
Citation
Electronic Proceedings in Theoretical Computer Science, EPTCS, 2014, 164, pp.33-47
ISSN
2075-2180
Start Page
33
End Page
47
Journal / Book Title
Electronic Proceedings in Theoretical Computer Science, EPTCS
Volume
164
Copyright Statement
© 2014 van Bakel and Vigliotti. This work is licensed under the Creative Commons Attribution License (https://creativecommons.org/licenses/by/3.0/)
License URL
Source
Fifth International Workshop on Classical Logic and Computation (CL&C 2014)
Subjects
cs.LO
cs.LO
F.3.2
Publication Status
Published
Start Date
2014-07-13
Coverage Spatial
Vienna, Austria
Date Publish Online
2014-09-11