## Algebraic Theories for Name-Passing Calculi

**Joachim Parrow and Davide Sangiorgi**
*Abstract:* In a theory of processes the names are atomic
data items which can be exchanged and tested for identity, but
which admit no other functions or predicates. A well-known example
of a calculus for name-passing is the pi-calculus, where names
additionally are used as communication ports. We provide complete
axiomatisations of late and early bisimulation equivalences in such
calculi. Since neither of the equivalences is a congruence we also
axiomatise the corresponding largest congruences. We consider a few
variations of the signature of the language; among these, a
calculus of deterministic processes which is reminiscent of
sequential functional programs with a conditional construct. Most
of our axioms are shown to be independent. The structure of the
systems reveals the symmetries of the calculi and equivalences
since they differ only by a few simple axioms.

*LFCS report ECS-LFCS-93-262,
April 1993.*

This report was published in *Information and Computation*,
**120**, pp174-197, August 1995.

Previous |

Index |

Next