Summary: This paper considers how locality restrictions on the use of capabilities can be enforced by a static type system. A distributed \(\pi\)-calculus with a simple reduction semantics is introduced, integrating location and migration primitives from the Distributed Join Calculus with asynchronous \(\pi\) 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. Subtyping allows all communications to be invoked uniformly. We show that the most local possible capabilities for internal channels can be inferred automatically.
For the entire collection see [Zbl 0893.00039].