Contracts for Mobile Processes

Abstract

Theories identifying well-formed systems of processes-those that are free of 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 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. © 2009 Springer Berlin Heidelberg.