-
Encapsulation and Dynamic Modularity in the Pi-Calculus
Authors:
Daniel Hirschkoff,
Aurélien Pardon,
Tom Hirschowitz,
Samuel Hym,
Damien Pous
Abstract:
We describe a process calculus featuring high level constructs for component-oriented programming in a distributed setting. We propose an extension of the higher-order pi-calculus intended to capture several important mechanisms related to component-based programming, such as dynamic update, reconfiguration and code migration. In this paper, we are primarily concerned with the possibility to bui…
▽ More
We describe a process calculus featuring high level constructs for component-oriented programming in a distributed setting. We propose an extension of the higher-order pi-calculus intended to capture several important mechanisms related to component-based programming, such as dynamic update, reconfiguration and code migration. In this paper, we are primarily concerned with the possibility to build a distributed implementation of our calculus. Accordingly, we define a low-level calculus, that describes how the high-level constructs are implemented, as well as details of the data structures manipulated at runtime. We also discuss current and future directions of research in relation to our analysis of component-based programming.
△ Less
Submitted 30 June, 2009;
originally announced June 2009.
-
Variable binding, symmetric monoidal closed theories, and bigraphs
Authors:
Richard Garner,
Tom Hirschowitz,
Aurélien Pardon
Abstract:
This paper investigates the use of symmetric monoidal closed (SMC) structure for representing syntax with variable binding, in particular for languages with linear aspects. In our setting, one first specifies an SMC theory T, which may express binding operations, in a way reminiscent from higher-order abstract syntax. This theory generates an SMC category S(T) whose morphisms are, in a sense, te…
▽ More
This paper investigates the use of symmetric monoidal closed (SMC) structure for representing syntax with variable binding, in particular for languages with linear aspects. In our setting, one first specifies an SMC theory T, which may express binding operations, in a way reminiscent from higher-order abstract syntax. This theory generates an SMC category S(T) whose morphisms are, in a sense, terms in the desired syntax. We apply our approach to Jensen and Milner's (abstract binding) bigraphs, which are linear w.r.t. processes. This leads to an alternative category of bigraphs, which we compare to the original.
△ Less
Submitted 26 May, 2009;
originally announced May 2009.
-
Graphical Presentations of Symmetric Monoidal Closed Theories
Authors:
Richard Garner,
Tom Hirschowitz,
Aurélien Pardon
Abstract:
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.
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.
△ Less
Submitted 8 June, 2009; v1 submitted 24 October, 2008;
originally announced October 2008.
-
Binding bigraphs as symmetric monoidal closed theories
Authors:
Tom Hirschowitz,
Aurélien Pardon
Abstract:
Milner's 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 syntax: given what we here call a bigraphical signature K, Milner constructs a (pre-) category of bigraphs BBig(K), whose main features are (1) the pr…
▽ More
Milner's 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 syntax: 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.
△ Less
Submitted 8 June, 2009; v1 submitted 24 October, 2008;
originally announced October 2008.
