Introduction to the PiCalculus


 An introductory course on process theory, via the medium of a
 particular process language. To be given at SEUJP-FC in the 2001/02
 academic year at the School of COGS, University of Sussex.  The course
 will last two days and is divided into four half day sessions. Each
 session will involve lectures followed by an exercise class in which
 attendees will solve problems using paper and pencil.
 
 Rationale
 ^^^^^^^^^
 Although the course is focused on a particular language the main aim
 is to expose attendees to some of the main concepts in concurrency theory. 
 We hope that at the end of the course attendees will be comfortable
 with the use of operational semantics for expressing the meaning of
 programs or processes, and will be able to carry out proofs using this 
 form of semantics.
 
 Prerequisites
 ^^^^^^^^^^^^^

 It is assumed that attendees are familiar with simple mathematical 
 proof techniques such as those covered in a first course in Discrete
 Maths. This should include the ability to carry out proofs by
 induction. A basic background in automata theory would also be useful.
 
 
 Session 1: Bisimulations
 ^^^^^^^^
 
 Bisimulation equivalences  form the core of most semantic theories 
 of processes. This session provides the necessary definitions and proof 
 techniques in an abstract setting.
 
 Labelled transition systems (lts) and their uses.
 
 Strong and weak bisimulation equivalences in arbitrary 
 labelled transition systems.
 
 Reasoning with Bisimulations.
 
 Deriving particular labelled transitions from the syntax 
 of a simple process language.
 
 Reduction semantics versus lts based semantics.
 
Proofs by rule induction.
 
 
 Session 2: The PiCalculus
 ^^^^^^^^^
 
 An Introduction to the PiCalculus, a process language 
 for describing systems with dynamic communication topologies.
 For didactic purposes we will use an asynchronous version of the
 language. 
 
 Informal examples.
 
 Reductions semantics and implementation of scope extrusion.
 
 Lts based semantics and resulting bisimulation equivalences.
 
 Synchronous versus asynchronous bisimulations.
 
Session 3: Types in the PiCalculus
 ^^^^^^^^^
 Types play an important role in  applications of the PiCalculus, 
 particularly as a target language for more more user-friendly 
 programming languages.
 
 Why are types needed ?
 
 A type inference system for simple types (Pierce-Sangiorgi types).
 
 
 Subject reduction and type safety.
 
 The effect of types on bisimulation equivalences. 
 
 Session 4: Algebraic Reasoning
 ^^^^^^^^^
 The syntax of the PiCalculus is based on a small set of algebraic 
 operators. This means that equivalences between processes can be 
 expressed via algebraic axioms or inference rules.
 
 Using algebraic laws and induction to proof process equivalences.
 
 Examples.
 
The algebraic laws for bisimulation equivalence.
 
 Soundness and Completeness of the laws.
 
 Reading:
 ^^^^^^^

 [1] R Milner, Communication and Concurrency, Prentice Hall, 1989.
 
 [2] R Milner, Communicating and mobile systems: the picalculus,
     Cambridge University Press, 1999.
 
 [3] J Parrow, An introduction to the piCalculus. Available from
     web-site.
 
 [4] D Sangiori and D Walker, The Pi-calculus: A Theory of mobile
     Processes, Cambridge University Press, 2001.