Contracts for Mobile Processes

Type theories identifying well-formed systems of processes—those that lack communication errors and enjoy strong properties such as deadlock freedom—are based either on session types, which are inhabited by channels, or on contracts, which are inhabited by processes. Current session type theories impose overly restrictive disciplines while contract theories, which do not suffer of such restrictions, only work for networks with fixed topology. Here we fill the gap between the two approaches by defining a theory of contracts for so-called mobile processes, those whose communications may include delegations and channel references. Althought contracts as defined here provide just a shallow abstraction of the behavior of processes they describe, this abstraction is enough to make our theory of contracts effective.