

Pi Calculus (Chapter 9), Peter Sewell.
pages 177197.
Cambridge University Press, December 2001.
ISBN 0521771846.
[ 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, Pictstyle 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 UCAMCLTR498, 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, Pictstyle 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 ]