11/04/2002: Glynn Winskel (Cambridge University Computer Laboratory)
Linearity and Nonlinearity in Distributed Computation

Résumé

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 path-based models of processes which are also models 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. Of course, process code can be sent explicitly to be copied. Following the discipline of linear logic, suitable nonlinear maps are obtained as linear maps whose domain is under an exponential. Different ways to make assemblies of processes lead to different choices of exponential; the nonlinear maps of only some of which will respect bisimulation.