Typed behavioural equivalences in the Pi calculus

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.