Domain Theory for Concurrency
Mikkel Nygaard
December 2003 |
Abstract:
A simple domain theory for concurrency is presented. Based on a
categorical model of linear logic and associated comonads, it highlights the
role of linearity in concurrent computation. Two choices of comonad yield two
expressive metalanguages for higher-order processes, both arising from
canonical constructions in the model. Their denotational semantics are fully
abstract with respect to contextual equivalence. One language derives from an
exponential of linear logic; it supports a straightforward operational
semantics with simple proofs of soundness and adequacy. The other choice of
comonad yields a model of affine-linear logic, and a process language with a
tensor operation to be understood as a parallel composition of independent
processes. The domain theory can be generalised to presheaf models, providing
a more refined treatment of nondeterministic branching. The article concludes
with a discussion of a broader programme of research, towards a fully fledged
domain theory for concurrency.
Available as PostScript, PDF, DVI. |