University of Cambridge


Typed behavioural equivalences in the Pi calculus

By Matthew Hennessy (COGS, University of Sussex)

We study typed behavioural equivalences for the Pi calculus, in which the type system allows a form of subtyping. This enables processes to selectively distribute different capabilities on communication channels. We show how typing, and more generally the inference rules used, affect the equivalences of processes.

The main result will be a co-inductive characterisation of a typed version of contextual equivalence between processes. The co-inductive characterisation uses a system of typed actions, which describes how type environments affect the actions which processes may perform.