Computer Laboratory

Technical reports

Applied π – a brief tutorial

Peter Sewell

July 2000, 65 pages

Abstract

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).

Full text

PDF (0.4 MB)
PS (0.2 MB)

BibTeX record

@TechReport{UCAM-CL-TR-498,
  author =	 {Sewell, Peter},
  title = 	 {{Applied $\pi$ -- a brief tutorial}},
  year = 	 2000,
  month = 	 jul,
  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-498.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-498}
}