# Strong bisimulation for explicit fusions

Lucian Wischik, Philippa Gardner.
FOSSACS 2004.

## Abstract.

The pi calculus holds the promise of compile-time checks for
whether a given program will have the correct interactive behaviour. The
theory behind such checks is called bisimulation. In the synchronous pi
calculus, it is well-known that the various natural definitions of (strong)
bisimulation yield different relations. In contrast, for the asynchronous pi
calculus, they collapse to a single relation. We show that the definitions
transfer naturally from the pi calculus to the explicit fusion calculus
(a symmetric variant of the synchronous pi calculus), where they also
collapse and yield a simpler theory.

The important property of an explicit fusion of names is that, in parallel
with a term, it allow the fused names to be substituted for each other.
This means that parallel contexts become as discriminating as arbitrary
contexts, and that open bisimilarity is more natural for the explicit fusion
calculus than it was for the pi calculus.

@InProceedings{gw04_explicit_fusion_bisimulation,
author = "Lucian Wischik and Philippa Gardner",
title = "Strong Bisimulation for Explicit Fusions",
booktitle = "FOSSACS 2004",
year = 2004,
editor = ???,
volume = ???,
pages = ???,
series = "Lecture Notes in Computer Science",
publisher = "Springer-Verlag",
url = "http:// www.wischik.com/ lu/ research/ eft.html",
}