Communicating Automata and Pi Calculus

Lecturer: Prof. A.J.R.G. Milner (rm135@cl.cam.ac.uk)

No. of lectures: 16

Prequisites: No formal prerequisites, but it is desirable to have attended one or other of Semantics of Programming Languages or Foundations of Functional Programming  

Communicating automata.

Examples of synchronised interaction; concurrent combination of automata; observation equivalence of automata; calculus of communicating systems (CCS) and its algebraic properties; examples of non-trivial concurrent systems and their analysis.

Introduction to pi calculus.

Examples of systems with dynamic reconfiguration, and their presentation; formal syntax of the pi calculus; rationale for this new basic model.

Basic theory of pi calculus.

Reaction rules and transition rules; bisimulation equivalence and congruence; comparison with other computational calculi; deriving properties of replication and recursion.

Practical application of pi calculus.

PICT, a programming language; programming in PICT; proofs of simple properties of realistic systems (e.g. operating systems) using pi calculus; `objects' as pi calculus agents.

Further topics.

Sorts, the type discipline of pi calculus; theoretical soundness of sorting; sorts in applications; functional programming as an application; the higher-order pi calculus.

Recommended texts (optional):

Milner, R. (1993). The polyadic pi calculus: a tutorial. In Logic and Algebra of Specification (ed. Bauer, F.L., Brauer, W. & Schwichtenberg, H.). Springer-Verlag.

Schwichtenberg, H. (1993). NATO ASI Series, Series F: Computer and Systems Sciences, vol. 94, pp. 203-246. Springer-Verlag.

Milner, R. (1989). Communication and Concurrency. Prentice-Hall.