BRICS, Dept. of Computer Science,
University of Aarhus
Teaching ·
Lecture notes ·
Research papers ·
Contact information ·
|
|
Mikkel Nygaard Ravn, PhD BRICS, Dept. of Computer Science, University of Aarhus |
Home · Teaching · Lecture notes · Research papers · Contact information · |
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.
© Elsevier 2004 (online
access)
Concurrent computation can be given an abstract mathematical treatment very similar to that provided for sequential computation by domain theory and denotational semantics of Scott and Strachey.
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, called HOPLA for Higher-Order Process LAnguage, derives from an exponential of linear logic. It can be viewed as an extension of the lambda calculus with CCS-like nondeterministic sum and prefix operations, in which types express the form of computation path of which a process is capable. HOPLA can directly encode calculi like CCS, CCS with process passing, and mobile ambients with public names, and it can be given a straightforward operational semantics supporting a standard bisimulation congruence. The denotational and operational semantics are related with simple proofs of soundness and adequacy. Full abstraction implies that contextual equivalence coincides with logical equivalence for a fragment of Hennessy-Milner logic, linking up with simulation equivalence.
The other language is called Affine HOPLA and is based on a weakening comonad that yields a model of affine-linear logic. This language adds to HOPLA an interesting tensor operation at the price of linearity constraints on the occurrences of variables. The tensor can be understood as a parallel composition of independent processes, and allows Affine HOPLA to encode processes of the kind found in treatments of nondeterministic dataflow.
The domain theory can be generalised to presheaf models, providing a more refined treatment of nondeterministic branching and supporting notions of bisimulation. The operational semantics for HOPLA is guided by the idea that derivations of transitions in the operational semantics should correspond to elements of the presheaf denotations. Similar guidelines lead to an operational semantics for the first-order fragment of Affine HOPLA. An extension of the operational semantics to the full language is based on a stable denotational semantics which associates to each computation path the minimal input necessary for that computation. Such a semantics is provided, based on event structures; it agrees with the presheaf semantics at first order and exposes the tensor operation as a simple parallel composition of event structures.
The categorical model obtained from presheaves is very rich in structure and points towards more expressive languages than HOPLA and Affine HOPLA - in particular concerning extensions to cover independence models. The thesis concludes with a discussion of related work towards a fully fledged domain theory for concurrency.
Revised version (December 4th 2003) [ ps.gz | pdf ]
Presentation at public
defence (November 21st 2003) [ pdf ]
Proof of
strong correspondence for HOPLA (August 7th 2004) [ ps | pdf ]
Operational semantics for Affine HOPLA (August 27th 2005)
[ txt ]
A fully abstract denotational semantics for the higher-order process language HOPLA is presented. It characterises contextual and logical equivalence, the latter linking up with simulation. The semantics is a clean, domain-theoretic description of processes as downwards-closed sets of computation paths: the operations of HOPLA arise as syntactic encodings of canonical constructions on such sets; full abstraction is a direct consequence of expressiveness with respect to computation paths; and simple proofs of soundness and adequacy shows correspondence between the denotational and operational semantics.
© Springer-Verlag 2003 (online
access)
Revised version [ ps | pdf ]
A small but powerful language for higher-order nondeterministic processes is introduced. Its roots in a linear domain theory for concurrency are sketched though for the most part it lends itself to a more operational account. The language can be viewed as an extension of the lambda calculus with a "prefixed sum", in which types express the form of computation path of which a process is capable. Its operational semantics, bisimulation, congruence properties and expressive power are explored; in particular, it is shown how it can directly encode process languages such as CCS, CCS with process passing, and mobile ambients with public names.
© Springer-Verlag 2002 (online
access)
Revised version [ ps | pdf ]
Please note: Paul Blain Levy seems to have found a problem with the way we use Howe's method to prove that bisimilarity is a congruence, and also to have fixed the proof in his 2006 paper Infinitary Howe's Method, (ENTCS 164).
The meaning and mathematical consequences of linearity (managing without a presumed ability to copy) 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, automatically respecting open-map bisimulation, in which a range of process operations can be expressed. An operational semantics is provided for the tensor fragment of the language. Different ways to make assemblies of processes lead to different choices of exponential, some of which respect bisimulation.
© IEEE 2002 (online access)
Revised version [ ps | pdf ]
This document reports on progress towards an operational understanding of presheaf models. With their built in notion of open-map bisimulation, presheaf models have been put forward as providing a domain theory for concurrency. An accompanying metalanguage in which terms are interpreted by profunctors between partial orders (with closed terms denoting presheaves) has been proposed by Winskel. Our contributions fall in two parts: First, we give an SOS style operational semantics to a first-order fragment of the metalanguage and establish an isomorphism between derivations and elements of presheaves. Second, by representing the profunctors that interpret open terms with prime event structures, a new denotational semantics of the same fragment is given. With this representation, elements of presheaves can be understood as configurations of event structures with prime configurations corresponding to the derivations of the operational semantics.
Original report [ ps | pdf ]
Correction [ ps | pdf ]
| Updated November 22nd, 2009. |
 
|