Global/local subtyping and capability inference for a distributed \(\pi\)-calculus. (English) Zbl 0910.03021

Sewell, Peter

Larsen, Kim G. (ed.) et al., Automata, languages and programming. 25th international colloquium, ICALP ’98. Aalborg, Denmark, July 13–17, 1998. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1443, 695-706 (1998).

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].

MSC:

03B70	Logic in computer science
68N01	General topics in the theory of software

Keywords:

subtyping; locality restrictions; static type system; distributed \(\pi\)-calculus; Distributed Join Calculus; asynchronous \(\pi\) communication; input and output capabilities of channels