Logic in Computer Science (LICS 2002)

Paper: Linearity in Distributed Computation (at LICS 2002)

Authors: Mikkel Nygaard Hansen Glynn Winskel

Abstract

The copying of processes is limited in the context of distributed computation, either as a fact of life, often because remote networks are simply too complicated to have control over, or deliberately, as in the design of security protocols. Roughly, linearity is about how to manage without a presumed ability to copy. The meaning and mathematical consequences of linearity are studied for a path-based model of processes which is also a model of affine-linear logic. This connection yields an affine-linear language for processes in which processes are typed according to the kind of computation paths they can perform. One consequence is that the affine-linear language automatically respects open-map bisimulation. A range of process operations (from CCS, CCS with process-passing, ambients, and dataflow) can be expressed within the affine-linear language showing the ubiquity of linearity. An operational semantics is provided for the tensor fragment of the language, and it is indicated how to understand the tensor operation as a parallel composition of event structures. Of course, process code can be sent explicitly to be copied. Different ways to make assemblies of processes lead to different choices of exponential, some of which respect bisimulation.

BibTeX

  @InProceedings{NygaardHansenWinske-LinearityinDistribu,
    author = 	 {Mikkel Nygaard Hansen and Glynn Winskel},
    title = 	 {Linearity in Distributed Computation},
    booktitle =  {Proceedings of the Seventeenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2002},
    year =	 2002,
    editor =	 {Gordon Plotkin},
    month =	 {July}, 
    location =   {Copenhagen, Denmark}, 
    publisher =	 {IEEE Computer Society Press}
  }