## Free-Algebra Models for the π-Calculus

In Foundations of Software Science and Computation Structures:
Proceedings of the 8th International Conference FOSSACS 2005, Edinburgh, UK, April 4–6, 2005,
Lecture Notes in Computer Science 3441, pages 155–169. Springer-Verlag, 2005.

Fetch the paper and slides from the conference presentation.
Go to other papers, talks or home page.

### Abstract

The finite π-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 π-calculus, and validate an existing construction as the
universal such model.

The algebraic operations are intuitive, covering name creation,
communication of names over channels, and nondeterminism; 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, and in particular allows us to use nonstandard arities that vary
as processes evolve.

Based on our algebraic theory we describe a category of models for the
π-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.

@InProceedings{stark:freamp,
author = {Ian Stark},
title = {Free-Algebra Models for the $\pi$-Calculus},
booktitle = {Foundations of Software Science and Computation Structures:
Proceedings of FOSSACS 2005},
pages = {155--169},
year = 2005,
number = 3441,
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
url = {http://www.inf.ed.ac.uk/~stark/freamp.html},
pdf = {http://www.inf.ed.ac.uk/~stark/freamp.pdf}
}

#### Page last modified:
Tuesday 5 August 2008