Nobuko Yoshida and Matthew Hennessy
 

In wide area distributed systems it is now common for
higher-order code to be transferred from one domain to another;
the receiving host may initialise parameters and then execute the code
in its local environment. In this paper we propose a fine-grained
typing system for a higher-order pi-calculus which can be used to
control the effect of such migrating code on local environments.
Processes may be assigned different types depending on their intended
use. This is in contrast to most of the previous work on typing
processes where all processes are typed by a unique constant type,
indicating essentially that they are well-typed relative to a
particular environment. Our fine-grained typing facilitates the
management of access rights and provides host protection from
potentially malicious behaviour.

Our process type takes the form of an interface limiting the
resources to which it has access, and the types at which they may be
used. Allowing resource names to appear both in process types and
process terms, as interaction ports, complicates the typing system
considerably. For the development of a coherent typing system, we use
a kinding technique, similar to that used by the subtyping of the
system F, and order-theoretic properties of our subtyping relation.

Various examples of this paper illustrate the usage of our
fine-grained process types in distributed systems.