In previous work with Pous, we defined a semantics for CCS which may both be viewed as an innocent form of presheaf semantics and as a concurrent form of game semantics. We define in this setting an analogue of fair testing equivalence, which we prov
e fully abstract w.r.t. standard fair testing equivalence. The proof relies on a new algebraic notion called playground, which represents the `rule of the game. From any playground, we derive two languages equipped with labelled transition systems, as well as a strong, functional bisimulation between them.
We define a semantics for Milners pi-calculus, with three main novelties. First, it provides a fully-abstract model for fair testing equivalence, whereas previous semantics covered variants of bisimilarity and the may and must testing equivalences. S
econd, it is based on reduction semantics, whereas previous semantics were based on labelled transition systems. Finally, it has a strong game semantical flavor in the sense of Hyland-Ong and Nickau. Indeed, our model may both be viewed as an innocent presheaf semantics and as a concurrent game semantics.
We propose a semantics for permutation equivalence in higher-order rewriting. This semantics takes place in cartesian closed 2-categories, and is proved sound and complete.
In previous work with Pous, we defined a semantics for CCS which may both be viewed as an innocent presheaf semantics and as a concurrent game semantics. It is here proved that a behavioural equivalence induced by this semantics on CCS processes is f
ully abstract for fair testing equivalence. The proof relies on a new algebraic notion called playground, which represents the rule of the game. From any playground, two languages, equipped with labelled transition systems, are derived, as well as a strong, functional bisimulation between them.
Milners bigraphs are a general framework for reasoning about distributed and concurrent programming languages. Notably, it has been designed to encompass both the pi-calculus and the Ambient calculus. This paper is only concerned with bigraphical syn
tax: given what we here call a bigraphical signature K, Milner constructs a (pre-) category of bigraphs BBig(K), whose main features are (1) the presence of relative pushouts (RPOs), which makes them well-behaved w.r.t. bisimulations, and that (2) the so-called structural equations become equalities. Examples of the latter include, e.g., in pi and Ambient, renaming of bound variables, associativity and commutativity of parallel composition, or scope extrusion for restricted names. Also, bigraphs follow a scoping discipline ensuring that, roughly, bound variables never escape their scope. Here, we reconstruct bigraphs using a standard categorical tool: symmetric monoidal closed (SMC) theories. Our theory enforces the same scoping discipline as bigraphs, as a direct property of SMC structure. Furthermore, it elucidates the slightly mysterious status of so-called links in bigraphs. Finally, our category is also considerably larger than the category of bigraphs, notably encompassing in the same framework terms and a flexible form of higher-order contexts.
We define a notion of symmetric monoidal closed (SMC) theory, consisting of a SMC signature augmented with equations, and describe the classifying categories of such theories in terms of proof nets.
