## Domain theory for concurrency

Glynn Winskel Computer Laboratory

#### Description

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.
Gian Luca Cattani and I have worked on 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 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.

#### 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.
(Used in the category-theory study group.)
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.