Global/local subtyping and capability inference for a distributed π-calculus

Abstract

This paper considers how locality restrictions on the use of capabilities can be enforced by a static type system. A distributed π-calculus with a simple reduction semantics is introduced, integrating location and migration primitives from the Distributed Join Calculus with asynchronous π communication. It is given a type system in which the input and output capabilities of channels may be either global, local or absent. This allows compile-time optimization where possible but retains the expressiveness of channel communication. Sub-typing allows all communications to be invoked uniformly. We show that the most local possible capabilities for internal channels can be inferred automatically.