## The Polyadic pi-Calculus: A Tutorial

**Robin Milner**
*Abstract:* The pi-calculus is a model of concurrent
computation based upon the notion of *naming*. It is first
presented in its simplest and original form, with the help of
several illustrative applications. Then it is generalized from
*monadic* to *polyadic* form. Semantics is done in terms
of both a reduction system and a version of labelled transitions
called *commitment*; the known algebraic axiomatization of
strong bisimilarity is given in the new setting, and so also is a
characterization in modal logic. Some theorems about the
*replication* operator are proved.

Justification for the polyadic form is provided by the concept
of *sort*, *sorting* and *sort discipline* which it
supports. Several illustrations of different sortings are given.
One example is the presentation of data structures as processes
which respect a particular sorting; another is the sorting for a
known translation of the lambda-calculus in to pi-calculus. For
this translation, the equational validity of beta-conversion is
proved with the help of replication theorems. The paper ends with
an extension of the pi-calculus to *w*-order processes, and a
brief account of the demonstration by Davide Sangiorgi that
higher-order processes may be faithfully encoded at first-order.
This extends and strengthens the original result of this kind given
by Bent Thomsen for second-order processes.

*LFCS report
ECS-LFCS-91-180*

This report was published in F. L. Hamer, W. Brauer and H.
Schwichtenberg, editors, *Logic and Algebra of
Specification*. Springer-Verlag, 1993.

Previous |

Index |

Next