

Global/Local Subtyping and Capability Inference for a
Distributed πcalculus.
Peter Sewell.
In ICALP 1998, (The link is to an extended version).
[ bib 
DOI 
ps 
pdf 
http ]
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 compiletime 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.


Global/Local Subtyping for a Distributed
πcalculus.
Peter Sewell.
Technical Report UCAMCLTR435, Computer Laboratory, University of
Cambridge, August 1997.
57pp.
[ bib 
ps (cmr) 
ps 
pdf 
.html ]
In the design of mobile agent programming languages there is a tension between the implementation cost and the expressiveness of the communication mechanisms provided. This paper gives a static type system for a distributed picalculus in which the input and output capabilities of channels may be either global or local. This allows compiletime optimization where possible but retains the expressiveness of channel communication. Subtyping allows all communications to be invoked uniformly. Recursive types and products are included. The distributed picalculus used integrates location and migration primitives from the Distributed Join Calculus with asynchronous pi communication, taking a simple reduction semantics. Some alternative calculi are discussed.