BRICS RS-98-31 G. Winskel: A Linear Metalanguage for Concurrency BRICS

Basic Research in Computer Science

A Linear Metalanguage for Concurrency

Glynn Winskel BRICS Report Series RS-98-31 ISSN 0909-0878 November 1998 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1998, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/98/31/

A Linear Metalanguage for Concurrency^{⋆}

Glynn Winskel

BRICS^{⋆⋆}, University of Aarhus, Denmark

Abstract. A metalanguage for concurrent process languages is introduced. Within it a range of process languages can be defined, including higher-order process languages where processes are passed and received as arguments. (The process language has, however, to be linear, in the sense that a process received as an argument can be run at most once, and not include name generation as in the Pi-Calculus.) The metalanguage is provided with two interpretations both of which can be understood as categorical models of a variant of linear logic. One interpretation is in a simple category of nondeterministic domains; here a process will denote its set of traces. The other interpretation, obtained by direct analogy with the nondeterministic domains, is in a category of presheaf categories; the nondeterministic branching behaviour of a process is captured in its denotation as a presheaf. Every presheaf category possesses a notion of (open-map) bisimulation, preserved by terms of the metalanguage. The conclusion summarises open problems and lines of future work.

1 Introduction

Over the last few years, Gian Luca Cattani and I have worked on presheaf models for interacting processes, culminating in Cattani’s forthcoming PhD thesis [3]. The work started from the general definition of bisimulation via open maps in [13] which suggested examining a broad class of models for concurrency—presheaf categories. Later we realised that presheaf models can themselves be usefully assembled together in a category in which the maps are colimit-preserving functors. There are two main benefits: one is a general result stating that colimit-preserving functors between presheaf categories preserve open maps and bisimulation [6]; the other that the category of the presheaf models is a form of domain theory for concurrency, with a compositional account of bisimulation, though at the cost that domains are categories rather than special partial orders [20, 4].

⋆ Invited paper AMAST ’98, Brazil ⋆⋆ Basic Research in CS, Centre of the Danish National Research Foundation.

We originally concentrated on the category of presheaf categories with colimit-preserving functors (or equivalently, the bicategory of profunctors). We’ve come to realise that by shifting category, to presheaf categories with connected-colimit preserving functors, a lot of our work can be done more systematically. (A connected colimit is a colimit of a nonempty connected diagram.) In particular the new category supports a metalanguage in which many of our constructions can be defined once and for all. This is not the only way the metalanguage saves work. Its terms will automatically preserve connected colimits. The metalanguage supports recursive definitions because ω-colimits are examples of connected colimits. Connectedcolimit preserving functors preserve open-map bisimulation. Consequently terms of the metalanguage preserve open-map bisimulation; if two terms which are open-map bisimilar are substituted for the same variable in a term of the metalanguage then the resulting terms will be open-map bisimilar.

The metalanguage can be interpreted in a wide range of categories. To spare some of the overhead of working with presheaf categories the metalanguage will first be interpreted in a simple category of nondeterministic domains. Equality of terms in this model will coincide with trace equivalence. However the nondeterministic domains are mathematically close to presheaf categories. With a switch of viewpoint, essentially the same constructions lead to an interpretation of the metalanguage in presheaf categories with connectedcolimit preserving functors, for which open-map bisimulation is an appropriate equivalence.

2 Presheaf models sketched

Let ℙ be a small category. The category of presheaves over ℙ, written ℙ̂, is the category [ℙ^{op}, Set] with objects the functors from ℙ^{op} (the opposite category) to Set (the category of sets and functions) and maps the natural transformations between them.

In our applications, the category ℙ is thought of as consisting of abstract paths (or computation-path shapes) where a map e : p → p′ expresses how the path p is extended to the path p′. In this paper the categories over which we take presheaves will be (the category presentation of) partial orders; the way a path p extends to a path p′ will be unique and a map from a path p to a path p′ simply a witness to p ≤ p′ in the partial order.

A presheaf X : ℙ^{op} → Set specifies for a typical path p the set X(p) of computation paths of shape p. The presheaf X acts on e : p → p′ in ℙ to give a function X(e) saying how p′-paths in X restrict to p-paths in X. In this way a presheaf can model the nondeterministic branching of a process.

Bisimulation on presheaves is derived from notion of open map between presheaves [12, 13]. Open maps are a generalisation of functional bisimulations, or zig-zag morphisms, known from transition systems [13]. Presheaves in ℙ̂ are bisimilar iff there is a span of surjective (i.e., epi) open maps between them.

Because the category of presheaves ℙ̂ is characterised abstractly as the free colimit completion of ℙ we expect that colimit-preserving functors between presheaf categories to be useful. They are, but not all operations associated with process languages preserve arbitrary colimits. Prefixing operations only preserve connected colimits while parallel compositions usually only preserve connected colimits in each argument separately. However, the preservation of connected colimits is all we need of a functor between presheaf categories for it to preserve bisimulation.

Proposition 1. [7] Let G : ℙ̂ → ℚ̂ be any connected-colimit preserving functor between presheaf categories. Then G preserves surjective open maps and open-map bisimulation.

Define Con to be the category consisting of objects partial orders ℙ, ℚ, ⋯, with maps g : ℙ → ℚ the connected-colimit preserving functors g : ℙ̂ → ℚ̂ between the associated presheaf categories, and composition the usual composition of functors. Define Col to be the subcategory of colimit-preserving functors.

3 Categories of nondeterministic domains

We obtain nondeterministic domains by imitating the definitions on presheaves but replacing Set by the much simpler partial order category 2 with two elements 0, 1 ordered by 0 ≤ 1.

Instead of presheaves ℙ̂ = [ℙ^{op}, Set] we now obtain ℙ̂ = [ℙ^{op}, 2], functors, and so monotonic functions from ℙ^{op} to 2. It’s not hard to see that an object x of ℙ̂ corresponds to a downwards-closed set given by {p ∈ ℙ | x(p) = 1}, and that a natural transformation from x to y in ℙ̂ corresponds to the inclusion of {p ∈ ℙ | x(p) = 1} in {p ∈ ℙ | y(p) = 1}. So we can identify ℙ̂ with the partial order of downwards-closed subsets of ℙ, ordered by inclusion. Thought of in this way it is sensible to think of ℙ̂ as a nondeterministic domain in the sense of [10, 9]; the order ℙ̂ has joins got simply via unions so it is certainly a cpo, with least element ∅, and we can think of the union operation as being a form of nondeterministic sum. It’s worth remarking that the domains obtained in this way are precisely the infinitely-distributive algebraic lattices (see e.g. [18, 19]) and that these are just the same as the prime algebraic lattices of [17], and free join completions of partial orders.

There are several choices about what to take as maps between nondeterministic domains. If we eschew “fairness”, the most generous we seem to have call for is that of all Scott-continuous functions between the domains. We are interested in maps which are just broad enough to include those operations we associate with interacting processes, operations such prefixing of actions, nondeterministic sum and parallel composition, so we look for a narrower class of maps than continuous functions.

3.1 The category Dom_{s}

On mathematical grounds it is natural to consider taking maps between nondeterministic domains which preserve their join structure, to choose functions f from ℙ̂ to ℚ̂ which preserve all joins, i.e. so f(⋃ X) = ⋃_{x∈X} f(x). Such functions (known often as additive functions) compose as usual, have identities and give rise to a category rich in structure. Call this category Dom_{s} and write f : ℙ →_{s} ℚ for a map in Dom_{s}, standing for an additive function from ℙ̂ to ℚ̂. Notice that such maps can be presented in several different ways. Because such maps preserve joins they are determined by their results on just the “complete primes”, elements p ↓ ∈ ℙ̂, for p ∈ ℙ, such that

p ↓(p′) = 1 if p′ ≤ p, and 0 otherwise.

Let f : ℙ →_{s} ℚ, so f : ℙ̂ → ℚ̂, and write f^{o} : ℙ → ℚ̂ for its restriction such that f^{o}(p) = f(p ↓), for p ∈ ℙ. As every element x of ℙ̂ is the join ⋃_{p∈x} p ↓ we see that

f(x) = ⋃_{p∈x} f^{o}(p) .

In this way maps f : ℙ →_{s} ℚ correspond to monotonic functions f^{o} : ℙ → ℚ̂. But monotonic functions g : ℙ → ℚ̂ are just the same as monotonic functions g : ℙ → [ℚ^{op}, 2] and, uncurrying, these correspond to monotonic functions h : ℙ × ℚ^{op} → 2 and so to elements of { \atop ℙ^{op} × ℚ} = [(ℙ^{op} ×ℚ)^{op}, 2]. This suggests that ℙ^{op} ×ℚ is a function space, as indeed is so.

The category Dom_{s} is monoidal-closed and in fact carries enough structure to be a categorical model of classical linear logic, the involution of linear logic, ℙ^{⊥}, being given as ℙ^{op}. The tensor of ℙ and ℚ is given by the product of partial orders ℙ × ℚ and the function space from ℙ to ℚ by ℙ^{op} × ℚ. Its products and coproducts are both given by disjoint unions on objects; for example the usual product of domains ℙ̂ × ℚ̂ is easily seen to be isomorphic to { \atop ℙ + ℚ}, the nondeterministic domain of the disjoint union ℙ + ℚ.

3.2 Lifting

One important construction on domains, that of lifting, is missing. Lifting a domain places a new bottom element below a domain. We can achieve this by adjoining a new element ⊥ below a copy of ℙ to obtain ℙ_{⊥}; a way to realise this is by taking ⊥ to be the empty set ∅ and the copy of ℙ to be {p ↓ | p ∈ ℙ} so that the order of ℙ_{⊥} is given simply by restricting the order of ℙ̂. Operations on processes, notably prefixing and parallel composition, make essential use of an operation associated with lifting. The operation is the function

⌊−⌋ : ℙ̂ → ℙ̂_{⊥}

such that ⌊x⌋(⊥) = 1 and ⌊x⌋(p ↓) = x(p) for x ∈ ℙ̂. But the function ⌊−⌋ is not a map from ℙ to ℙ_{⊥} in Dom_{s} as it does not preserve all joins; the problem occurs with the join of the empty set ⋃ ∅, the least element of ℙ̂, which is not sent to the least element of ℙ̂_{⊥}.

3.3 The category Dom

To accommodate the function ⌊−⌋ we are forced to move to a slightly broader category, though fortunately one that inherits a good many properties from Dom_{s}. The category Dom has the same objects, partial orders, but its morphisms from ℙ to ℚ, written f : ℙ → ℚ, are functions f : ℙ̂ → ℚ̂ which need only preserve nonempty joins, or more accurately, joins of non-empty sets.

Maps ℙ → ℚ in Dom are determined by their action on ∅ and p ↓, for p ∈ ℙ. This is because any x ∈ ℙ̂ is trivially the nonempty join with the least element ∅ ∪ ⋃_{p∈x} p ↓. Given the way to represent ℙ_{⊥} as consisting precisely of the elements ∅ and p ↓, for p ∈ ℙ, there is an embedding j : ℙ_{⊥} → ℙ̂. So any map f : ℙ → ℚ is determined by its restriction f ∘ j : ℙ_{⊥} → ℚ̂. The restriction f ∘ j is clearly monotonic. Moreover any monotonic function g : ℙ_{⊥} → ℚ̂ has an extension^{1} g^{†} : ℙ → ℚ in Dom given by g^{†}(x) = ⋃_{p∈⌊x⌋} g(p ↓) for x ∈ ℙ̂. The two operations (−) ∘ j and (−)^{†} are mutually inverse. Consequently maps ℙ → ℚ in Dom correspond bijectively to maps ℙ_{⊥} →_{s} ℚ in Dom_{s},^{2} and so to elements in { \atop (ℙ_{⊥})^{op} × ℚ}.

3.4 Fixed points

The set of maps in Dom from a path order ℙ to one ℚ inherits an order from elements of the function space { \atop (ℙ_{⊥})^{op} × ℚ}. Operations of the category Dom will come to preserve nonempty joins of such maps and, in particular, joins of ω-chains. Hence operations F of Dom taking maps ℙ → ℚ to maps ℙ → ℚ will have least fixed points fix F : ℙ → ℚ.

3.5 Intuition

How is one to think of the category Dom? The interpretation we’ll give and the way in which we define denotational semantics to process languages will have some novelty, though similar uses of categories of nondeterministic domains have been made (see for instance

1 In fact, the left Kan extension along j. 2 The correspondence is natural in ℙ and ℚ making Dom the coKliesli category asso-

ciated to the comonad (−)_{⊥} on Dom_{s} and a reflective subcategory of Dom_{s}.

[10, 9]). An object ℙ is to be thought of as consisting of finite computation paths (each one a “trace” in the sense of [11]), for example the finite string of actions that a CCS or CSP process might perform. The partial order p ≤ p′ on ℙ is thought of as saying that the computation path p can be extended to the computation path p′. With this intuition in mind we shall call the objects of Dom path orders. An element of ℙ̂ is a trace set as in [11] and stands for the set of computation paths a nondeterministic process can perform.

A map f : ℙ → ℚ takes a nondeterministic process with computation paths in ℙ as input and yields a nonderministic process with computation paths in ℚ as output. How is one to understand that a map preserves joins of nonempty sets? Because the map need only preserve nonempty joins it is at liberty to ignore the input process in giving nontrivial output. Because the map preserves all nonempty joins the interaction with the input process has to be conducted in a linear way; the input process cannot be copied to explore its different nondeterministic possibilities, so once started it can only follow a single course of computation, during which it may be interacted with intermittently. It’s helpful to think of a map in Dom as a context which surrounds an input process interacting with the input process occasionally and sometimes interacting with its own environment; whichever computation path the output process (the context surrounding the input process) follows it can only involve the input process following a single computation path.

4 Constructions on path orders

4.1 Tensor

The tensor of path orders ℙ ⊗ ℚ is given by the set (ℙ_{⊥} × ℚ_{⊥}) \ {(⊥, ⊥)}, ordered coordinatewise, in other words, as the product of ℙ_{⊥} and ℚ_{⊥} as partial orders but with the bottom element (⊥, ⊥) removed.

Let f : ℙ → ℙ′ and g : ℚ → ℚ′. We define f ⊗g : ℙ⊗ℚ → ℙ′ ⊗ℚ′ as the extension (cf. Section 3.3) h^{†} of a monotonic function

h : (ℙ ⊗ ℚ)_{⊥} → { \atop ℙ′ ⊗ ℚ′} .

Notice that (ℙ ⊗ ℚ)_{⊥} is isomorphic to the product as partial orders of ℙ_{⊥} × ℚ_{⊥} in which the bottom element is then (⊥, ⊥). With this realisation of (ℙ ⊗ ℚ)_{⊥} we can define h : ℙ_{⊥} × ℚ_{⊥} → { \atop ℙ′ ⊗ ℚ′} by taking

(h(p, q))(p′, q′) = ⌊f(p)⌋(p′) × ⌊g(q)⌋(q′)

for p ∈ ℙ_{⊥}, q ∈ ℚ_{⊥} and (p′, q′) ∈ ℙ′ ⊗ ℚ′—on the right we use the product, or meet, of 2, so 0 × 0 = 0 × 1 = 1 × 0 = 0 and 1 × 1 = 1.

The unit for tensor is the empty path order 𝕆.

Elements x ∈ ℙ̂ correspond to maps x̃ : 𝕆 → ℙ sending the empty element to x. Given x ∈ ℙ̂ and y ∈ ℚ̂ we define x⊗y ∈ { \atop ℙ ⊗ ℚ} to be the element pointed to by x̃ ⊗ ỹ: 𝕆 → ℙ ⊗ ℚ.

4.2 Function space

The function space of path orders ℙ ⊸ ℚ is given by the product of partial orders (ℙ_{⊥})^{op} × ℚ. Thus the elements of ℙ ⊸ ℚ are pairs, which we write suggestively as (p ↦ q), with p ∈ ℙ_{⊥}, q ∈ ℚ, ordered by

(p′ ↦ q′) ≤ (p ↦ q) ⟺ p ≤ p′ & q′ ≤ q

—note the switch in order on the left.

We have the following chain of isomorphisms between partial orders:

ℙ ⊗ ℚ ⊸ ℝ = (ℙ ⊗ ℚ)_{⊥} × ℝ ≅ ℙ_{⊥} × ℚ_{⊥} × ℝ ≅ ℙ ⊸ (ℚ ⊸ ℝ) .

This gives isomorphism between the elements { \atop ℙ ⊗ ℚ ⊸ ℝ} and { \atop ℙ ⊸ (ℚ ⊸ ℝ)}. Thus there is a 1-1 correspondence curry from maps ℙ ⊗ ℚ → ℝ to maps ℙ → (ℚ ⊸ ℝ) in Dom; its inverse is called uncurry. We obtain linear application, app : (ℙ ⊸ ℚ) ⊗ ℙ → ℚ, as uncurry(1_{ℙ⊸ℚ}).

4.3 Products

The product of path orders ℙ&ℚ is given by the disjoint union of ℙ and ℚ. An element of { \atop ℙ&ℚ} can be identified with a pair (x, y), with x ∈ ℙ̂ and y ∈ ℚ̂, which provides the projections π_{1} : ℙ&ℚ → ℙ and π_{2} : ℙ&ℚ → ℚ. More general, not just binary, products &_{i∈I} ℙ_{i} with projections π_{j}, for j ∈ I, are defined similarly. From the universal property of products, a collection of maps f_{i} : ℙ → ℙ_{i}, for i ∈ I, can be tupled together to form a unique map ⟨f_{i}⟩_{i∈I} : ℙ → &_{i∈I} ℙ_{i} with the property that π_{j} ∘ ⟨f_{i}⟩_{i∈I} = f_{j} for all j ∈ I. The empty product is given by 𝕆 and as the terminal object is associated with unique maps ℙ → 𝕆, constantly ∅, for any path order ℙ. Finite products are most often written as ℙ_{1}& ⋯ &ℙ_{k}.

Each object ℙ is associated with (nondeterministic) sum operations, a map Σ : &_{i∈I} ℙ → ℙ in Dom taking an element of the domain, viewed as a tuple {x_{i} | i ∈ I}, to its union ⋃_{i∈I} x_{i} in ℙ̂. The empty sum yields ∅ ∈ ℙ. Finite sums are typically written as x_{1} + ⋯ + x_{k}.

Because there are empty elements we can define maps in Dom_{s} from products to tensors of path orders. For instance, in the binary case, σ : ℙ&ℚ →_{s} ℙ ⊗ ℚ in Dom_{s} is specified by

(x, y) ↦ (x ⊗ ∅) + (∅ ⊗ y) .

The composition of such a map with the diagonal map, viz.

ℙ ^{\underline{diag}}→ ℙ&ℙ ^{\underline{σ}}→ ℙ ⊗ ℙ

will play a role later in the semantics of the metalanguage, allowing us to duplicate arguments to maps of a certain kind.

4.4 Lifted sums

The category Dom does not have coproducts. However, we can build a useful sum in Dom with the help of the coproduct of Dom_{s} and lifting. Let ℙ_{i}, for i ∈ I, be a family of path orders. As their lifted sum we take the disjoint union of the path orders Σ_{i∈I}ℙ_{i}_{⊥}, over the underlying set ⋃_{i∈I}{i} × (ℙ_{i})_{⊥} ; the latter path order forms a coproduct in Dom_{s} with the obvious injections in_{j} : ℙ_{j}_{⊥} →_{s} Σ_{i∈I}ℙ_{i}_{⊥}, for j ∈ I. The injections In_{j} : ℙ_{j} → Σ_{i∈I}ℙ_{i}_{⊥} in Dom, for j ∈ I, are defined to be the composition In_{j}(−) = in_{j}(⌊−⌋). This construction is not a coproduct in Dom. However, it does satisfy a weaker property analogous to the universal property of a coproduct. Suppose f_{i} : ℙ_{i} → ℚ are maps in Dom for all i ∈ I. Then, there is a unique mediating map

f : Σ_{i∈I}ℙ_{i}_{⊥} →_{s} ℚ

in Dom_{s} (note the subscript) such that

f ∘ In_{i} = f_{i}

for all i ∈ I.

Suppose that the family of maps f_{i} : ℙ_{i} → ℚ, with i ∈ I, has the property that each f_{i} is constantly ∅ whenever i ∈ I is different from j and that f_{j} is h : ℙ_{j} → ℚ. Write [h]_{j} : ∑_{i∈I} ℙ_{i}_{⊥} → ℚ for the unique mediating map obtained for this choice. Then

[h]_{j}(In_{j}(z)) = h(z) , [h]_{j}(In_{i}(z)) = ∅ if i ≠ j , and [h]_{j}(∅) = ∅ .

For a general family f_{i} : ℙ_{i} → ℚ, with i ∈ I, we can describe the action of the mediating morphism on x ∈ { \atop Σ_{i∈I}ℙ_{i}_{⊥}} as f(x) = Σ_{i∈I}[f_{i}]_{i}(x).

Because lifted sum is not a coproduct we do not have that tensor distributes over lifted sum to within isomorphism. However there is a map in Dom_{s}

dist : ℚ ⊗ Σ_{i∈I}ℙ_{i}_{⊥} →_{s} Σ_{i∈I}(ℚ ⊗ ℙ_{i})_{⊥} ,

expressing a form of distributivity, given as the extension h^{†} of the function

h : ℚ_{⊥}×(Σ_{i∈I}ℙ_{i}_{⊥})_{⊥} → Σ_{i∈I}(ℚ⊗ℙ_{i})_{⊥}; h(q, (i, p)) = (i, (q, p)) ↓, h(q, ⊥) = ∅ .

Unary lifted sums in Dom, when I is a singleton, are an important special case as they amount to lifting.

4.5 Recursive definitions

Suppose that we wish to model a process language rather like CCS but where processes are passed instead of discrete values, subject to the linearity constraint that when a process is received it can be run at most once. Assume the synchronised communication occurs along channels forming the set A. The path orders can be expected to satisfy the following equations:

ℙ = ℙ_{⊥} + Σ_{a∈A}ℂ_{⊥} + Σ_{a∈A}𝔽_{⊥} ,  ℂ = ℙ ⊗ ℙ ,  𝔽 = (ℙ ⊸ ℙ) .

The three components of process paths ℙ represent paths beginning with a silent (τ) action, an output on a channel (a!), resuming as a concretion path (in ℂ), and an input from a channel (a?), resuming as an abstraction path (in 𝔽). It is our choice of path for abstractions which narrows us to a linear process-passing language, one where the input process can be run at most once to yield a single (computation) path.

Fortunately the simple technique for solving recursive domain equations via information systems in [14] suffices to solve such equations. A path order ℙ can be regarded as an information system in which every finite subset of ℙ is consistent and in which the entailment relation is given by the partial order ≤ of ℙ, so {p′} ⊢ p iff p ≤ p′. Path orders under the order

ℙ ⊴ ℚ ⟺ ℙ ⊆ ℚ & (∀p, p′ ∈ ℙ. p ≤_{ℙ} p′ ⟺ p ≤_{ℚ} p′)

form a (large) cpo with respect to which all the constructions on path orders we have just seen are continuous (their continuity is verified just as in information systems by showing them monotonic w.r.t. ⊴ and “continuous on token sets”). Solutions to equations like those above are then obtained as (simultaneous) least fixed points.

5 A metalanguage

Assume that path orders are presented using the constructions with the following syntax:

\begin{matrix}𝕋 ::= & 𝕆 | 𝕋_{1} ⊗ 𝕋_{2} | 𝕋_{1} ⊸ 𝕋_{2} | Σ_{i∈I}𝕋_{i}_{⊥} | 𝕋_{1}&𝕋_{2} \\ | P | μ_{j}P_{1}, ⋯, P_{k}.(𝕋_{1}, ⋯, 𝕋_{k}) \end{matrix}

All the construction names have been met earlier with the exception of the notation for recursively defined path orders. Above P is drawn from a set of variables used in the recursive definition of path orders; μ_{j}P_{1}, ⋯, P_{k}.(𝕋_{1}, ⋯, 𝕋_{k}) stands for the j-component (so 1 ≤ j ≤ k) of the ⊴-least solution to the defining equations

P_{1} = 𝕋_{1}, ⋯, P_{k} = 𝕋_{k} ,

in which the expressions 𝕋_{1}, ⋯, 𝕋_{k} may contain P_{1}, ⋯, P_{k}. We shall write μP_{1}, ⋯, P_{k}.(𝕋_{1}, ⋯, 𝕋_{k}) as an abbreviation for

(μ_{1}P_{1}, ⋯, P_{k}.(𝕋_{1}, ⋯, 𝕋_{k}), ⋯, μ_{k}P_{1}, ⋯, P_{k}.(𝕋_{1}, ⋯, 𝕋_{k})) .

In future we will often use vector notation and, for example, write μ\overrightarrow{P}.\overrightarrow{𝕋} for the expression above, and confuse a closed expression for a path order with the path order itself.

The operations of Sections 3 and 4 form the basis of a “raw” syntax of terms which will be subject to typing and linearity constraints later:

t, u, v, ⋯::= x, y, z, ⋯  (Variables)
∅ | Σ_{i∈I}t_{i} |  (Sums)
rec x.t |  (Recursive definitions)
λx.t | u · v |  (Abstraction and application)
In_{j}(t) | [t > In_{j}(x) ⇒ u] | (Injections and tests for lifted sums)
(t, u) | [t > (x, −) ⇒ u] |
[t > (−, x) ⇒ u] | (Pairing and tests for products)
t ⊗ u | [t > x ⊗ y ⇒ u]  (Tensor operation and tests)

The language is similar to that in [1], being based on a form of pattern matching. In particular [t > In_{j}(x) ⇒ u] “tests”or matches t denoting an element of a lifted sum against the pattern In_{j}(x) and passes the results of successful matches for x on to u; how the possibly multiple results of successful matches are combined to a final result varies according to the category in which language is interpreted. Accordingly, variables like x in such patterns are binding occurrences and bind later occurrences of the variable in the body, u in this case. We shall take for granted an understanding of free and bound variables, and substitution on raw terms. In examples we’ll allow ourselves to use + both in writing sums of terms and lifted sums of path orders.

Let ℙ_{1}, ⋯, ℙ_{k} be closed expressions for path orders and assume that the variables x_{1}, ⋯, x_{k} are distinct. A syntactic judgement

x_{1} : ℙ_{1}, ⋯, x_{k} : ℙ_{k} ⊢ t : ℚ

stands for a map

[[x_{1} : ℙ_{1}, ⋯, x_{k} : ℙ_{k} ⊢ t : ℚ]] : ℙ_{1} ⊗ ⋯ ⊗ ℙ_{k} → ℚ

in Dom. We shall typically write Γ, or Δ, for an environment list x_{1} : ℙ_{1}, ⋯, x_{k} : ℙ_{k}. We shall most often abbreviate the denotation map to

ℙ_{1} ⊗ ⋯ ⊗ ℙ_{k} ^{\underline{t}}→ ℚ , or even Γ ^{\underline{t}}→ ℚ .

Here k may be 0 so the list in the syntactic judgement is empty and the corresponding tensor product the empty path order 𝕆.

A linear language will restrict copying and so substitutions of a common term into distinct variables. The counterpart in the models is the absence of a suitable diagonal map from objects ℙ to ℙ ⊗ ℙ. For example the function x ↦ x⊗x from ℙ̂ to { \atop ℙ ⊗ ℙ} is not in general a map in Dom. To see this assume that ℙ is the discrete order on the set {a, b}. Then the nonempty join x = a ↓ ∪ b ↓ is not sent to

(a ↓ ⊗ a ↓) ∪ (b ↓ ⊗ b ↓) = {(a, a), (b, b), (a, ⊥), (⊥, b)}

as would be needed to preserve non-empty joins, but instead to

x ⊗ x = {(a, a), (b, b), (a, b), (a, ⊥), (⊥, b)}

with the extra “cross term” (a, b). Consider a term t(x, y), with its free variables x and y shown explicitly, for which

x : ℙ, y : ℙ ⊢ t(x, y) : ℚ ,

corresponding to a map ℙ ⊗ ℙ ^{\underline{t(x,y)}}→ ℚ in Dom. This does not generally entail that

x : ℙ ⊢ t(x, x) : ℚ

—there may not be a corresponding map in Dom, for example if t(x, y) = x ⊗ y. There is however a condition on how the variables x and y occur in t which ensures that the judgement x : ℙ ⊢ t(x, x) : ℚ holds and that it denotes the map in Dom obtained as the composition

ℙ ^{\underline{diag}}→ ℙ&ℙ ^{\underline{σ}}→ ℙ ⊗ ℙ ^{\underline{t(x,y)}}→ ℚ

—using the maps seen earlier in Section 4.3. Semantically, the map ℙ ⊗ ℙ ^{\underline{t(x,y)}}→ ℚ has to be essentially a map ℙ&ℙ → ℚ, more precisely the left Kan extension of such a map along σ. Syntactically, this is assured if the variables x and y are not crossed in t according to the following definition:

Definition 2. Let t be a raw term. Say a set of variables V is crossed in t iff there are subterms of t of the form

a tensor s ⊗ u, an application s · u, or a test [z > u ⇒ s]

for which t has free occurrences of variables from V appearing in both s and u.

For example, variables x and y are crossed in x ⊗ y, but variables x and y are not crossed in (x + y) ⊗ z. Note that a set of variables V is crossed in a term t if V contains variables x, y, not necessarily distinct, so that {x, y} is crossed in t. We are mainly interested in when sets of variables are not crossed in a term.

The term-formation rules are listed below alongside their interpretations as a constructors on morphisms, taking the morphisms denoted by the premises to that denoted by the conclusion (along the lines of [2]). We assume that the variables in any enviroment list which appears are distinct. Structural rules:

\overline{x : ℙ ⊢ x : ℙ} , interpreted as \overline{ℙ ^{\underline{1_{ℙ}}}→ ℙ} .

\frac{Δ ⊢ t : ℙ}{Γ, Δ ⊢ t : ℙ} , interpreted as \frac{Δ ^{\underline{t}}→ ℙ}{Γ ⊗ Δ ^{\underline{∅⊗1_{Γ}}}→ 𝕆 ⊗ Δ ≅ Δ ^{\underline{t}}→ ℙ} .
\frac{Γ, x : ℙ, y : ℚ, Δ ⊢ t : ℝ}{Γ, y : ℚ, x : ℙ, Δ ⊢ t : ℝ} , interpreted via s : ℚ ⊗ ℙ ≅ ℙ ⊗ ℚ as

\frac{Γ ⊗ ℙ ⊗ ℚ ⊗ Δ ^{\underline{t}}→ ℝ}{Γ ⊗ ℚ ⊗ ℙ ⊗ Δ ^{\underline{1_{Γ} ⊗s⊗1_{Δ}}}→ Γ ⊗ ℙ ⊗ ℚ ⊗ Δ ^{\underline{t}}→ ℝ} .

Recursive path orders:

\frac{Γ ⊢ t : 𝕋_{j}[μ\overrightarrow{P}.\overrightarrow{𝕋}/\overrightarrow{P}]}{Γ ⊢ t : μ_{j}\overrightarrow{P}.\overrightarrow{𝕋}} , \frac{Γ ⊢ t : μ_{j}\overrightarrow{P}.\overrightarrow{𝕋}}{Γ ⊢ t : 𝕋_{j}[μ\overrightarrow{P}.\overrightarrow{𝕋}/\overrightarrow{P}]} .

where the premise and conclusion of each rule are interpreted as the same map because μ_{j}\overrightarrow{P}.\overrightarrow{𝕋} and 𝕋_{j}[μ\overrightarrow{P}.\overrightarrow{𝕋}/\overrightarrow{P}] denote equal path orders. Sums of terms:

\overline{Γ ⊢ ∅ : ℙ} , interpreted as \overline{Γ ^{\underline{∅}}→ ℙ} , the constantly ∅ map.

\frac{Γ ⊢ t_{i} : ℙ for all i ∈ I}{Γ ⊢ Σ_{i∈I}t_{i} : ℙ} , interpreted as \frac{Γ ^{\underline{t_{i}}}→ ℙ for all i ∈ I}{Γ ^{\underline{⟨t_{i}⟩_{i∈I}}}→ &_{i∈I} ℙ ^{\underline{Σ}}→ ℙ} .

Recursive definitions:

\frac{Γ, x : ℙ ⊢ t : ℙ \{y, x\} not crossed for all y in Γ}{Γ ⊢ rec x.t : ℙ} , interpreted as \frac{Γ ⊗ ℙ ^{\underline{t}}→ ℙ}{Γ ^{\underline{fix F}}→ ℙ}

—see Section 3.4, where for Γ ^{\underline{g}}→ ℙ the map F (g) is the composition

Γ ^{\underline{diag}}→ Γ &Γ ^{\underline{σ}}→ Γ ⊗ Γ ^{\underline{1_{Γ} ⊗g}}→ Γ ⊗ ℙ ^{\underline{t}}→ ℙ .

Abstraction:

\frac{Γ, x : ℙ ⊢ t : ℚ}{Γ ⊢ λx.t : ℙ ⊸ ℚ} , interpreted as \frac{Γ ⊗ ℙ ^{\underline{t}}→ ℚ}{Γ ^{\underline{curry t}}→ (ℙ ⊸ ℚ)} .

Application:

\frac{Γ ⊢ u : ℙ ⊸ ℚ Δ ⊢ v : ℙ}{Γ, Δ ⊢ u · v : ℚ} ,interpreted as \frac{Γ ^{\underline{u}}→ (ℙ ⊸ ℚ) Δ ^{\underline{v}}→ ℙ}{Γ ⊗ Δ ^{\underline{u⊗v}}→ (ℙ ⊸ ℚ) ⊗ ℙ ^{\underline{app}}→ ℚ} .

Injections and test for lifted sums:

\frac{Γ ⊢ t : ℙ_{j} , where j ∈ I}{Γ ⊢ In_{j}(t) : Σ_{i∈I}ℙ_{i}_{⊥}} , interpreted as \frac{Γ ^{\underline{t}}→ ℙ_{j} , where j ∈ I}{Γ ^{\underline{t}}→ ℙ_{j} ^{\underline{In_{j}}}→ Σ_{i∈I}ℙ_{i}_{⊥}} .

\frac{Γ, x : ℙ_{j} ⊢ u : ℚ , where j ∈ I. Δ ⊢ t : ∑_{i∈I} ℙ_{i}_{⊥}}{Γ, Δ ⊢ [t > In_{j}(x) ⇒ u] : ℚ} , interpreted as

\frac{Γ ⊗ ℙ_{j} ^{\underline{u}}→ ℚ , where j ∈ I. Δ ^{\underline{t}}→ ∑_{i∈I} ℙ_{i}_{⊥}}{Γ ⊗ Δ ^{\underline{1_{Γ} ⊗t}}→ Γ ⊗ ∑_{i∈I} ℙ_{i}_{⊥} ^{\underline{dist}}→ ∑_{i∈I}(Γ ⊗ ℙ_{i})_{⊥} ^{\underline{[−]_{j}}}→ ℚ} .

Pairing and tests for products:

\frac{Γ ⊢ t : ℙ Γ ⊢ u : ℚ}{Γ ⊢ (t, u) : ℙ&ℚ} , interpreted as \frac{Γ ^{\underline{t}}→ ℙ Γ ^{\underline{u}}→ ℚ}{Γ ^{\underline{⟨t,u⟩}}→ ℙ&ℚ} .

\frac{Γ, x : ℙ ⊢ u : ℝ Δ ⊢ t : ℙ&ℚ}{Γ, Δ ⊢ [t > (x, −) ⇒ u] : ℝ}, interpreted as

\frac{Γ ⊗ ℙ ^{\underline{u}}→ ℝ Δ ^{\underline{t}}→ ℙ&ℚ}{Γ ⊗ Δ ^{\underline{1_{Γ} ⊗(π_{1}∘t)}}→ Γ ⊗ ℙ ^{\underline{u}}→ ℝ} .

\frac{Γ, x : ℚ ⊢ u : ℝ Δ ⊢ t : ℙ&ℚ}{Γ, Δ ⊢ [t > (−, x) ⇒ u] : ℝ}, interpreted as

\frac{Γ ⊗ ℚ ^{\underline{u}}→ ℝ Δ ^{\underline{t}}→ ℙ&ℚ}{Γ ⊗ Δ ^{\underline{1_{Γ} ⊗(π_{2}∘t)}}→ Γ ⊗ ℚ ^{\underline{u}}→ ℝ} .

Tensor operation and test for tensor:

\frac{Γ ⊢ t : ℙ Δ ⊢ u : ℚ}{Γ, Δ ⊢ t ⊗ u : ℙ ⊗ ℚ} , interpreted as \frac{Γ ^{\underline{t}}→ ℙ Δ ^{\underline{u}}→ ℚ}{Γ ⊗ Δ ^{\underline{t⊗u}}→ ℙ ⊗ ℚ} .
\frac{Γ, x : ℙ, y : ℚ ⊢ u : ℝ Δ ⊢ t : ℙ ⊗ ℚ}{Γ, Δ ⊢ [t > x ⊗ y ⇒ u] : ℝ}, interpreted as

\frac{Γ ⊗ ℙ ⊗ ℚ ^{\underline{u}}→ ℝ Δ ^{\underline{t}}→ ℙ ⊗ ℚ}{Γ ⊗ Δ ^{\underline{1_{Γ} ⊗t}}→ Γ ⊗ ℙ ⊗ ℚ ^{\underline{u}}→ ℝ} .

Proposition 3. Suppose Γ, x : ℙ ⊢ t : ℚ. The set {x} is not crossed in t.

Lemma 4. (Well-formed substitutions) Suppose

Γ, x_{1} : ℙ, ⋯, x_{k} : ℙ ⊢ t : ℚ

and that the set of variables {x_{1}, ⋯, x_{k}} is not crossed in t. Suppose Δ ⊢ u : ℙ where the variables of Γ and Δ are disjoint. Then,

Γ, Δ ⊢ t[u/x_{1}, ⋯, u/x_{k}] : ℚ .

In particular, as singleton sets of variables are not crossed in well-formed terms we immediately deduce:

Corollary 5. If Γ, x : ℙ ⊢ t : ℚ and Δ ⊢ u : ℙ, where the variables of Γ and Δ are disjoint, then Γ, Δ ⊢ t[u/x] : ℚ.

Exploiting the naturality of the various operations used in the semantic definitions, we can show:

Lemma 6. (Substitution Lemma) Suppose Γ, x : ℙ ⊢ t : ℚ and Δ ⊢ u : ℙ where Γ and Δ have disjoint variables. Then,

[[Γ, Δ ⊢ t[u/x] : ℚ]] = [[Γ, x : ℙ ⊢ t : ℚ]] ∘ (1_{Γ} ⊗ [[Δ ⊢ u : ℙ]]) .

In particular, linear application amounts to substitution:

Lemma 7. Suppose Γ ⊢ (λx.t) · u : ℚ. Then, Γ ⊢ t[u/x] : ℚ and

[[Γ ⊢ (λx.t) · u : ℚ]] = [[Γ ⊢ t[u/x] : ℚ]] .

5.1 Extending the metalanguage

General patterns are well-formed terms built up according to

p ::= x | ∅ | In_{j}(p) | p ⊗ q | (p, −) | (−, p) | p ↦ p′ .

A test on a pattern [u > p ⇒ t] binds the free variables of the pattern p to the resumptions after following the path specified by the pattern in u; because the term t may contain these variables freely the resumptions may influence the computation of t. Such a test is understood inductively as an abbreviation for a term in the metalanguage:

[u > x ⇒ t] ≡ (λx.t) · u , [u > ∅ ⇒ t] ≡ t , [u > In_{j}(p) ⇒ t] ≡ [u > In_{j}(x) ⇒ [x > p ⇒ t]] for a fresh variable x, [u > (p, −) ⇒ t] ≡ [u > (x, −) ⇒ [x > p ⇒ t]] for a fresh variable x, [u > (−, p) ⇒ t] ≡ [u > (−, x) ⇒ [x > p ⇒ t]] for a fresh variable x, [u > p ⊗ q ⇒ t] ≡ [u > x ⊗ y ⇒ [p > x ⇒ [q > y ⇒ t]]] for fresh variables x, y, [u > (p ↦ q) ⇒ t] ≡ [u > f ⇒ [f · p > q ⇒ t]] for a fresh variable f.

Let λx ⊗ y.t stand for λw.[w > x ⊗ y ⇒ t], where w is a fresh variable, and write [u_{1} > p_{1}, ⋯, u_{k} > p_{k} ⇒ t] to abbreviate [u_{1} > p_{1} ⇒ [⋯ [u_{k} > p_{k} ⇒ t] ⋯].

5.2 Interpretation in Con

We can interpret the metalanguage in the category of presheaf models Con with essentially the same constructions and operations as those in Dom, once we replace 2 by Set and understand (nonempty) joins as (connected) colimits; ^{3} the category of presheaf models Col will play the role of Dom_{s}. Because now domains [ℙ^{op}, 2] are replaced by presheaf categories [ℙ^{op}, Set] we shall often have to make do with isomorphism rather than straight equality.

In fact, to mimic the mathematics behind the interpretation of the metalanguage in Dom, all that’s required of a category V, in place of 2, is that it has all colimits and all finite products. Now ℙ̂,

3 A function between partial orders with least elements preserves (connected) colimits iff it preserves (nonempty) joins.

taken to be [ℙ^{op}, V], will have all colimits, in particular coproducts to interpret (nondeterministic) sums, and will also support left Kan extensions to play the role of (−)^{†}. We can understand the embedding (−) ↓ : ℙ → ℙ̂ through the initial and terminal objects 0 and 1 of V. The lifting map ⌊−⌋ : ℙ → ℙ̂, again defined so ⌊x⌋(⊥) = 1 and ⌊x⌋(p ↓) = x(p), will preserve connected colimits. Using the product of V, instead of that of 2, we can copy the definition of the functor ⊗.

The advantage of this generality is that objects in the category V don’t just have to say whether a path is present in a process but can provide a “measure” of how. If V is Set a process will denote a presheaf X which identifies the set of different ways X(p) in which a path p is realised.

6 Examples

6.1 CCS

As in CCS, assume a set of labels A, a complementation operation producing ā from a label a, with ¯ ā = a, and a distinct label τ. In the metalanguage we can specify the path order ℙ as the ⊴-least solution

ℙ = ℙ_{⊥} + Σ_{a∈A}ℙ_{⊥} + Σ_{a∈A}ℙ_{⊥} .

Write the injections from ℙ into its expression as a lifted sum as τ.t, a.t and ā.t for a ∈ A and term t of type ℙ. The curried CCS parallel composition can be defined as the following term of type ℙ ⊸ (ℙ ⊸ ℙ) in the metalanguage:

P ar = rec P. λxλy. Σ_{α∈A∪{τ}}[x > α.x′ ⇒ α.(P · x′ · y)]+
Σ_{α∈A∪{τ}}[y > α.y′ ⇒ α.(P · x · y′)]+

Σ_{a∈A}[x > a.x′, y > ā.y′ ⇒ τ.(P · x′ · y′)] .

The other CCS operations are easy to encode. Interpreted in Dom two CCS terms will have the same denotation iff they have same traces (or execution sequences). By virtue of having been written down in the metalanguage the operation of parallel composition will preserve open-map bisimulation when interpreted in Con; for this specific ℙ, open-map bisimulation coincides with strong bisimulation.

In Con we can recover the expansion law for general reasons: the Substitution Lemmas 6,7 hold in Con, though with isomorphism replacing equality; the mediating morphism associated with lifted sums are now in Col (the analogue of Dom_{s}) so that tests for lifted sums distribute over nondeterministic sums. In more detail, write X|Y for P ar · X · Y, where X and Y are terms of type ℙ. Suppose

X = Σ_{α∈A∪{τ}}Σ_{i∈I(α)}α.X_{i} , Y = Σ_{α∈A∪{τ}}Σ_{j∈J(α)}α.Y_{j} .

Using Lemma 7, and then that the tests distribute over nondeterministic sums,

X|Y ≅Σ_{α∈A∪{τ}}[X > α.x′ ⇒ α.(x′|Y)] + Σ_{α∈A∪{τ}}[Y > α.y′ ⇒ α.(X|y′)]
+ Σ_{a∈A}[X > a.x′, Y > ā.y′ ⇒ τ.(x′|y′)]
≅Σ_{α∈A∪{τ}}Σ_{i∈I(α)}α.(X_{i}|Y) + Σ_{α∈A∪{τ}}Σ_{j∈J(α)}α.(X|Y_{j})
+ Σ_{a∈A}Σ_{i∈I(a),j∈J(ā)}τ.(X_{i}|Y_{j}) .

The equation for the path order for CCS with early value-passing would be very similar to that above. An equation suitable for late value-passing is

ℙ = ℙ_{⊥} + Σ_{a∈A,v∈V} ℙ_{⊥} + Σ_{a∈A}(Σ_{v∈V} ℙ_{⊥})_{⊥} ,

though this is not the same equation as in [20] which has Σ_{a∈A}(Σ_{v∈V} ℙ)_{⊥} as the final component—perhaps the metalanguage should be broadened to allow this.

6.2 A linear higher-order process language

Recall the path orders for processes, concretions and abstractions for a higher-order language in Section 4.5. We are chiefly interested in the parallel composition of processes, P ar_{ℙ,ℙ} of type ℙ⊗ℙ ⊸ ℙ. But parallel composition is really a family of mutually dependent operations also including components such as P ar_{𝔽,ℂ} of type 𝔽 ⊗ ℂ ⊸ 𝔽 to say how abstractions compose in parallel with concretions etc. All these components can be tupled together in a product using &, and parallel composition defined as a simultaneous recursive definition whose component at ℙ ⊗ ℙ ⊸ ℙ satisfies

P |Q =Σ_{α}[P > α.P′ ⇒ α(P′|Q)]+
Σ_{α}[Q > α.Q′ ⇒ α(P |Q′)]+
Σ_{a}[P > a?F, Q > a!S ⊗ R ⇒ τ.(F · S|R)]+
Σ_{a}[P > a!S ⊗ R, Q > a?F ⇒ τ.(R|F · S)] ,

where we have chosen suggestive names for the injections and, for instance, P |Q abbreviates P ar_{ℙ,ℙ}·(P ⊗Q). In the summations a ∈ A and α ranges over a!, a?, τ for a ∈ A.

7 Problems

The interpretation of the metalanguage in Con provides a base from which to examine its equational theory and operational semantics. We should update the treatment of bisimulation in [4] to take better account of Con and the metalanguage.

The range of interpretations for the metalanguage indicated in Section 5.2 is restrictive, for example, in requiring V to be cocomplete. As remarked in [8] there are sensible choices for V which are not cocomplete—the countable sets for instance, provided we also restrict the path orders to be countable.

Perhaps instantiating V to some specific category, can help provide a “presheaf model” of a higher-order Pi-Calculus to accompany [5]. This would be a good basis from which to compare and relate with the project of action structures [16].

The metalanguage here cries out for extensions in two directions, one to cope with name generation as in the Pi-Calculus, the other to go beyond linearity. The exponential ! of [20, 5] seems appropriate but its effects on open-map bisimulation are not understood.

The question of how to approach higher-order independence models remains.

How to turn the framework on weak bisimulation and contextual equivalence is the subject of current work based on a lead by Marcelo Fiore.

Gian Luca Cattani and I are working on how to understand openmap bisimulation at higher-order in operational terms [7].

References

1. S. Abramsky. Computational interpretation of linear logic. Tech. Report 90/20, Dept. of Computing, Imperial College, 1990.

2. T. Braüner. An Axiomatic Approach to Adequacy. BRICS Dissertation Series DS-96-4, 1996.

3. G. L. Cattani. Forthcoming PhD thesis, CS Dept., University of Aarhus.

4. G. L. Cattani, M. Fiore, and G. Winskel. A Theory of Recursive Domains with Applications to Concurrency. In Proc. of LICS ’98.

5. G. L. Cattani, I. Stark, and G. Winskel. Presheaf Models for the π-Calculus. In Proc. of CTCS ’97, LNCS 1290, 1997.

6. G. L. Cattani and G. Winskel. Presheaf Models for Concurrency. In Proc. of CSL’ 96, LNCS 1258, 1997.

7. G. L. Cattani and G. Winskel. On bisimulation for higher order processes. Manuscript, 1998.

8. G. L. Cattani, A. J. Power and G. Winskel. A categorical axiomatics for bisimulation. In Proc. of CONCUR’98, LNCS 1466, 1998.

9. M. Hennessy. A fully abstract denotational semantics for the pi-calculus Computer Science Technical Report 96:04, Sussex University, 1996.

10. M. Hennessy and G.D. Plotkin. Full abstraction for a simple parallel programming language. In Proc. of MFCS’79, LNCS 74, 1979.

11. C.A.R. Hoare. A model for communicating sequential processes. Tech. Report PRG-22, University of Oxford Computing Lab., 1981.

12. A. Joyal and I. Moerdijk. A completeness theorem for open maps. Annals of Pure and Applied Logic, 70:51–86, 1994.

13. A. Joyal, M. Nielsen, and G. Winskel. Bisimulation from open maps. Information and Computation, 127:164–185, 1996.

14. G.Winskel and K.Larsen. Using information systems to solve recursive domain equations effectively. LNCS 173, 1984.

15. R. Milner. Communication and concurrency. Prentice Hall, 1989.

16. R. Milner. Calculi for Interaction. Acta Informatica 33, 1996.

17. M. Nielsen, G.D. Plotkin and G. Winskel. Petri nets, Event structures and Domains, part 1. Theoretical Computer Science, vol. 13, 1981.

18. G. Winskel. A representation of completely distributive algebraic lattices. Report of the Computer Science Dept., Carnegie-Mellon University, 1983.

19. G. Winskel. An introduction to event structures. In Proc. of REX summerschool in temporal logic, ’May 88, LNCS 354, 1988.

20. G. Winskel. A presheaf semantics of value-passing processes. In Proceedings of CONCUR’96, LNCS 1119, 1996.

Recent BRICS Report Series Publications

RS-98-31 Glynn Winskel. A Linear Metalanguage for Concurrency. November 1998. 21 pp.

RS-98-30 Carsten Butz. Finitely Presented Heyting Algebras. November 1998. 30 pp.

RS-98-29 Jan Camenisch and Markus Michels. Proving in Zero-Knowledge that a Number is the Product of Two Safe Primes. November 1998. 19 pp.

RS-98-28 Rasmus Pagh. Low Redundancy in Dictionaries with O(1) Worst Case Lookup Time. November 1998. 15 pp.

RS-98-27 Jan Camenisch and Markus Michels. A Group Signature Scheme Based on an RSA-Variant. November 1998. 18 pp. Preliminary version appeared in Ohta and Pei, editors, Advances in Cryptology: 4th ASIACRYPT Conference on the Theory and Applications of Cryptologic Techniques, ASIACRYPT ’98 Proceedings, LNCS 1514, 1998, pages 160–174.

RS-98-26 Paola Quaglia and David Walker. On Encoding pπ in mπ. October 1998. 27 pp. Full version of paper to appear in Foundations of Software Technology and Theoretical Computer Science: 18th Conference, FCT&TCS ’98 Proceedings, LNCS, 1998.

RS-98-25 Devdatt P. Dubhashi. Talagrand’s Inequality in Hereditary Settings. October 1998. 22 pp.

RS-98-24 Devdatt P. Dubhashi. Talagrand’s Inequality and Locality in Distributed Computing. October 1998. 14 pp.

RS-98-23 Devdatt P. Dubhashi. Martingales and Locality in Distributed Computing. October 1998. 19 pp.

RS-98-22 Gian Luca Cattani, John Power, and Glynn Winskel. A Categorical Axiomatics for Bisimulation. September 1998. ii+21 pp. Appears in Sangiorgi and de Simone, editors, Concurrency Theory: 9th International Conference, CONCUR ’98 Proceedings, LNCS 1466, 1998, pages 581–596.

RS-98-21 John Power, Gian Luca Cattani, and Glynn Winskel. A Representation Result for Free Cocompletions. September 1998. 16 pp.