Bisimulation in name-passing calculi without matching
- 27 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- No. 10436871,p. 165-175
- https://doi.org/10.1109/lics.1998.705653
Abstract
We study barbed equivalence in name-passing languages where there is no matching construct for testing equality between names. We concentrate on the /spl pi/-calculus with capability types and subtypes, of which the untyped /spl pi/-calculus without matching is a special case. We give a coinductive characterisation of typed barbed equivalence, and present "bisimulation up-to" techniques to enhance the resulting coinductive proof method. We then use these techniques to prove some process equalities that fail in the ordinary /spl pi/-calculus.Keywords
This publication has 13 references indexed in Scilit:
- A calculus of mobile processes, IPublished by Elsevier ,2004
- Typing and subtyping for mobile processesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Imperative objects as mobile processesScience of Computer Programming, 2002
- Bisimulations in the Join-CalculusPublished by Springer Nature ,1998
- Behavioral equivalence in the polymorphic pi-calculusPublished by Association for Computing Machinery (ACM) ,1997
- Linearity and the pi-calculusPublished by Association for Computing Machinery (ACM) ,1996
- On reduction-based process semanticsTheoretical Computer Science, 1995
- On the proof method for bisimulationLecture Notes in Computer Science, 1995
- On asynchronous communication semanticsPublished by Springer Nature ,1992
- Compositionality Through an Operational Semantics of ContextsJournal of Logic and Computation, 1991