11/04/2002: Glynn Winskel (Cambridge University Computer Laboratory)
Domain theory for concurrency

Résumé

Classical domain theory and denotational semantics, started by Strachey and Scott, has been quite inspirational in suggesting programming languages, their types and ways to understand them. They have played a much lesser role in research in interactive/concurrent/distributed computation. One reason perhaps is that classical domain theory has not scaled up to the more intricate models we find used in concurrency.
The course will move towards a path-based domain theory for interacting processes, one aim being a general theory of bisimulation, also for higher-order process languages. This mini-course, structured as a series of lectures, will explain the origins of this work and the ideas and mathematics on which it rests.
The first lecture should be very accessible and give a gentle introduction to the advantages of viewing models for concurrency as categories, in which the arrows are forms of simulation. It will show how many operations of process algebra arise as universal constructions in a category and introduce a general definition of bisimulation based on ``open maps''. The lecture will be mainly based on the familiar model of labelled transition systems, but will indicate how the ideas are equally applicable to other models such as event structures and Petri nets, and how relations between different models are often expressed as adjunctions.
The following lectures will introduce and motivate a broader space of models of concurrent computation, leading to a form of domain theory for concurrency, in which nondeterministic processes are represented by presheaves; the role of domain will be replaced by that of presheaf category. There are several ways to introduce presheaves, but this course will emphasise the guiding intuition that presheaves are a form of transition system which allow computation paths to have a variety of forms. Bisimulation between presheaves is again obtained from open maps. Here a useful theorem is that colimit-preserving functors between presheaf categories preserve open maps, and so bisimulation. Its proof will be presented, helped some of the way by the view of presheaves as transition systems.
Finally, I hope to give an idea of the languages for concurrency and the concepts of linearity and nonlinearity the mathematics suggests. The prior PPS seminar on April 11 should help in giving a general overview.

References:
The relevant mathematics can be found in: Mario Ca'ccamo and Glynn Winskel. Lecture Notes on Category Theory. Inspired by a Mathematics Part III course of Martin Hyland. See http://www.brics.dk/~mcaccamo.
An introduction to open maps in: Andre' Joyal, Mogens Nielsen, and Glynn Winskel. Bisimulation from Open Maps. May 1994. 42 pp. Appears in LICS '93 special issue of Information and Computation, 127(2):164-185, June 1986. An early version is obtainable from: http://www.brics.dk/RS/94/Ref/BRICS-RS-94-Ref/BRICS-RS-94-Ref.html.
A discussion of different models for concurrency in: Glynn Winskel and Mogens Nielsen. Models for Concurrency. May 1994. 144 pp. Appears as a chapter in the Handbook of Logic and the Foundations of Computer Science, vol. 4, pages 1-148, Oxford University Press, 1995.
First ideas on the suggested languages in: Glynn Winskel. A linear metalanguage for concurrency. Invited lecture in proc. AMAST'98, Brazil, Springer Lecture Notes in CS, vol. 1548, 1999. Obtainable from: http://www.brics.dk/RS/98/Ref/BRICS-RS-98-Ref/BRICS-RS-98-Ref.html.