Binding bigraphs as symmetric monoidal closed theories

Milner's bigraphs [1] are a general framework for reasoning about distributed and concurrent programming languages. Notably, it has been designed to encompass both the -calculus [2] and the Ambient calculus [3]. This paper is only concerned with bigraphical syntax: given what we here call a bigraphical signature K, Milner constructs a (pre-) category of bigraphs Bbg(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 are, e.g., in and Ambients, renaming of bound variables, associativity and commutativity of parallel composition, or scope extrusion for -bound 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 disci...

• Type: Journal
• Year: 2008
• Where: CORR
• Authors: Tom Hirschowitz, Aurélien Pardon
• Keywords: Bound Variables, Concurrent Programming Languages, CORR 2008, Education, So-called Structural Equations