Logic in Computer Science (LICS 2000)

Paper: Assigning Types to Processes (at LICS 2000)

Authors: Nobuko Yoshida Matthew Hennessy

Abstract

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 initialize 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 a unique constant type, indicating essentially that they are well typed relative to a particular environment, types all processes.Our process type takes a 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 in both 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 use of our fine-grained typing system for distributed systems. As a specific application, we define a new typed behavioral equivalence for the higher-order pi-calculus. The expressiveness of our types enables us to state and prove interesting identities between typed processes.

BibTeX

  @InProceedings{YoshidaHennessy-AssigningTypestoPro,
    author = 	 {Nobuko Yoshida and Matthew Hennessy},
    title = 	 {Assigning Types to Processes},
    booktitle =  {Proceedings of the Fifteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2000},
    year =	 2000,
    editor =	 {Martin Abadi},
    month =	 {June}, 
    pages =      {334--345},
    location =   {Santa Barbara, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }