Binding bigraphs as symmetric monoidal closed theories

12 years 9 months ago
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...
Tom Hirschowitz, Aurélien Pardon
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2008
Where CORR
Authors Tom Hirschowitz, Aurélien Pardon
Comments (0)