Typed behavioural equivalences for processes in the presence of subtyping

Abstract

We study typed behavioural equivalences for the -calculus in which the type system allows a form of subtyping. This enables processes to distribute different capabilities selectively on communication channels. The equivalences considered include typed versions of testing equivalences and barbed bisimulation equivalences.We show that each of these equivalences can be characterised via standard techniques applied to a novel labelled transition system of configurations. These consist of a process term together with two related type environments; one constraining the process and the other its computing environment.