Bisimulations in the join-calculus

We develop a theory of bisimulations in the join-calculus. We introduce a r efined operational model that makes interactions with the environment expli cit, and discuss the impact of the lexical scope discipline of the join-cal culus on its extensional semantics. We propose several formulations of bisi mulation and 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 matching. (C) 2001 Elsevier Sci ence B.V. All rights reserved.