JavaScript is disabled for your browser. Some features of this site may not work without it.

## Metatheory of the $\pi$-Calculus

#####
**Author**

Weber, Sam; Bloom, Bard

#####
**Abstract**

Milner's {$\pi$}-calculus is a very influential process algebra in which communication channels are first-class objects. One of the basic concepts in the language is the transmission of one channel along another. This leads to immensely powerful programming techniques, which have been used for modelling things from cellular telephones to object-oriented languages. However, the {$\pi$}-calculus lacks many operations, such as broadcasting a value to many processes, interrupting processes, checkpointing, and even such basics as sequencing and \t{while}-loops in full generality. Adding all useful operations to the {$\pi$}-calculus would make it unusably large and complex. We thus propose a \e{rule format}, called \metapi. The {$\pi$}-calculus, and a vast range of other calculi treating channels as first-class data, can be expressed with {\metapi} rules. Any operations defined by {\metapi} rules have the same essential theory as the {$\pi$}-calculus. For example, all such operations respect the appropriate notion of strong bisimulation. Furthermore, the {$\pi$}-calculus, and all the operations in the previous paragraph, have {\metapi} equivalents. {\metapi} describes the heart of the {$\pi$}-calculus without prejudice towards the particular communication mechanisms of the calculus, and thus gives a general framework for working with {$\pi$}-like calculi. Further, it can be argued that the {\metapi} rule format is the most general of its kind, in the sense that any obvious extensions to the format would cause important language properties to be violated.

#####
**Date Issued**

1996-01#####
**Publisher**

Cornell University

#####
**Subject**

computer science; technical report

#####
**Previously Published As**

http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR96-1564

#####
**Type**

technical report