Bisimulations in the Join-Calculus
Michele Boreale, Cédric Fournet, Cosimo Laneve · 1998
We develop a theory of bisimulation in the join-calculus. We introduce a refined operational model that makes interactions with the environment explicit, and we discuss the impact of the lexical discipline of the join-calculus on its extensional semantics. We propose several formulations of bisimulation and we establish that all formulations yield the same equivalence. We prove that this equivalence is finer than barbed congruence, but that both relations coincide in the presence of name-testing.