The Polyadic π-Calculus: a Tutorial

Robin Milner

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract

The π-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 concepts of sort and sorting 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 λ-calculus into π-calculus. For this translation, the equational validity of β-conversion is proved with the help of replication theorems. The paper ends with an extension of the π-calculus to ω-order processes, and a brief account of the demonstration by Sangiorgi [27] that higher-order processes may be faithfully encoded at first-order. This extends and strengthens the original result of this kind given by Thomsen [28] for second-order processes.
Original languageUndefined/Unknown
Title of host publicationLogic and Algebra of Specification
Subtitle of host publicationNATO ASI Series
EditorsFriedrichL. Bauer, Wilfried Brauer, Helmut Schwichtenberg
PublisherSpringer Berlin Heidelberg
Pages203-246
Number of pages44
Volume94
ISBN (Electronic)978-3-642-58041-3
ISBN (Print)978-3-642-63448-2
DOIs
Publication statusPublished - 1993

Publication series

NameNATO ASI Series
PublisherSpringer Berlin Heidelberg

Keywords

  • bisimulation
  • concurrency
  • communication
  • data structures
  • higher-order processes
  • ?-calculus
  • mobile processes
  • naming
  • parallel computation
  • process algebra
  • process logic
  • reduction system
  • sort

Cite this