Pi Calculus

Origin. Milner, Parrow, Walker (1992). Mobile processes. Channel passing. Name binding. Foundation for mobile computation.

Models. Processes exchange channel names. Dynamic reconfiguration. Name scope extrusion. Bisimulation over mobile systems.

Formalism.

Syntax: P ::= 0 | x̄⟨y⟩.P | x(z).P | P | Q | (νx)P | !P | P + Q

Output: x̄⟨y⟩.P: send y on x, then P. Channel x, message y.

Input: x(z).P: receive on x, bind to z. z bound in P.

Parallel: P | Q: concurrent.

Restriction: (νx)P: fresh private name x. Scope of x is P.

Replication: !P = P | P | P | ... Unbounded copies.

Communication: x̄⟨y⟩.P | x(z).Q →τ P | Q[y/z] Synchronous.

Scope extrusion: (νx)(x̄⟨x⟩.P | R) | x(z).Q →τ (νx)(P | R | Q[x/z]) Private name escapes scope.

Structural congruence: P | 0 ≡ P P | Q ≡ Q | P (νx)0 ≡ 0 (νx)(νy)P ≡ (νy)(νx)P

Bisimulation: Late vs early. Open bisimulation. Congruence properties.

Symbols.

Symbol	Unicode	Name	Meaning
x̄⟨y⟩	—	Output	Send y on x
x(z)	—	Input	Receive, bind z
(νx)	U+03BD	New	Fresh name
!	—	Replication	Unbounded
≡	U+2261	Congruent	Structurally equal

Metatheory. Turing complete. Bisimulation congruence (with care). Encodings of λ-calculus. Type systems for linearity.

Applies to. Mobile systems. Web services. Security protocols. Concurrent objects. Distributed systems.

Limitations. Complexity. Name management. Bisimulation subtle. Infinite state.