Series: Penn State Logic Seminar

Date: Tuesday, April 11, 2000

Speaker: Philippa Gardner, Cambridge University, Computer Science

Title: A Process Calculus With Explicit Fusions

Time: 2:30 - 3:20 PM

Place: 219 Thomas Building

Abstract: 

We introduce the pi_F-calculus, a pi-calculus based on explicit
fusions. The explicit fusion x=y is a process which declares that two
names can be used interchangeably. In contrast, the fusion calculus of
Parrow and Victor treats fusions implicitly as part of the reaction
relation.  We give simple embeddings of the pi, the pi_I and the
fusion calculus, and prove a full abstraction result which connects
bisimulation for the pi-calculus with bisimulation for its embedding
in the pi_F-calculus.

We will explore two equivalent bisimulation congruences. One arises
from a standard labelled transition system (LTS), in which a label can
be regarded as an offer of a synchronisation with an external
process. The other arises from a new form of LTS, in which a label
denotes a small context necessary to create a redex. Both definitions
of bisimulation provide a natural analysis of the graphical structure
of processes.

This talk describes joint work with Lucian Wischik, and arose from our
previous work on process frameworks. A basic knowledge of the
pi-calculus is assumed.