Chapter 9, Pi Calculus, in the book Formal Methods for Distributed Processing, A Survey of Object Oriented Approaches, edited by Howard Bowman and John Derrick, Peter Sewell. pages 177--197. Cambridge University Press, December 2001. ISBN 0521771846. The links are to the TR498 extended version of the book chapter. [ bib | ps | pdf ]
This note provides a brief introduction to π-calculi and their application to concurrent and distributed programming. Chapter 1 introduces a simple π-calculus and discusses the choice of primitives, operational semantics (in terms of reductions and of indexed early labelled transitions), operational equivalences, Pict-style programming and typing. Chapter 2 goes on to discuss the application of these ideas to distributed systems, looking informally at the design of distributed π-calculi with grouping and interaction primitives. Chapter 3 returns to typing, giving precise definitions for a simple type system and soundness results for the labelled transition semantics. Finally, Chapters 4 and 5 provide a model development of the metatheory, giving first an outline and then detailed proofs of the results stated earlier. The note can be read in the partial order 1.(2+3+4.5).

 
Applied π -- A Brief Tutorial. Peter Sewell. Technical Report UCAM-CL-TR-498, Computer Laboratory, University of Cambridge, August 2000. 65pp. [ bib | ps | pdf | .html ]
This note provides a brief introduction to π-calculi and their application to concurrent and distributed programming. Chapter 1 introduces a simple π-calculus and discusses the choice of primitives, operational semantics (in terms of reductions and of indexed early labelled transitions), operational equivalences, Pict-style programming and typing. Chapter 2 goes on to discuss the application of these ideas to distributed systems, looking informally at the design of distributed π-calculi with grouping and interaction primitives. Chapter 3 returns to typing, giving precise definitions for a simple type system and soundness results for the labelled transition semantics. Finally, Chapters 4 and 5 provide a model development of the metatheory, giving first an outline and then detailed proofs of the results stated earlier. The note can be read in the partial order 1.(2+3+4.5).

 
A Brief Introduction to Applied π, Peter Sewell, January 1999. Lecture notes for the Mathfit Instructional Meeting on Recent Advances in Semantics and Types for Concurrency: Theory and Practice, July 1998. [ bib | .html ]