Informatics Report Series


Report   

EDI-INF-RR-1207


Related Pages

Report (by Number) Index
Report (by Date) Index
Author Index
Institute Index

Home
Title:Free-Algebra Models for the Pi-Calculus
Authors: Ian Stark
Date: 2007
Publication Title:Theoretical Computer Science
Publisher:Elsevier
Publication Type:Journal Article Publication Status:Published
DOI:10.1016/j.tcs.2007.09.024
Abstract:
The finite pi-calculus has an explicit set-theoretic functor- category model that is known to be fully abstract for strong late bisimulation congruence. We characterize this as the initial free algebra for an appropriate set of operations and equations in the enriched Lawvere theories of Plotkin and Power. Thus we obtain a novel algebraic description for models of the pi-calculus, and validate an existing construction as the universal such model. <p> The algebraic operations are intuitive, covering name creation, communication of names over channels, and nondeterministic choice; the equations then combine these features in a modular fashion. We work in an enriched setting, over a "possible worlds" category of sets indexed by available names. This expands significantly on the classical notion of algebraic theories: we can specify operations that act only on fresh names, or have arities that vary as processes evolve. <p> Based on our algebraic theory of pi we describe a category of models for the pi-calculus, and show that they all preserve bisimulation congruence. We develop a direct construction of free models in this category; and generalise previous results to prove that all free-algebra models are fully abstract. We show how local modifications to the theory can give alternative models for pi-I and the early pi-calculus. <p> From this theory of pi we also obtain a Moggi-style computational monad, suitable for a programming language semantics of mobile communicating systems. This addresses the challenging area of correctly combining computational monads: in this case those for for concurrency, name generation, and communication.
Links To Paper
Page by publisher
Bibtex format
@Article{EDI-INF-RR-1207,
author = { Ian Stark },
title = {Free-Algebra Models for the Pi-Calculus},
journal = {Theoretical Computer Science},
publisher = {Elsevier},
year = 2007,
doi = {10.1016/j.tcs.2007.09.024},
url = {http://dx.doi.org/10.1016/j.tcs.2007.09.024},
}


Home : Publications : Report 

Please mail <reports@inf.ed.ac.uk> with any changes or corrections.
Unless explicitly stated otherwise, all material is copyright The University of Edinburgh