CIS 700: π-Calculus and Foundations of Concurrent Systems
Spring 2004

Instructors: Benjamin Pierce & Steve Zdancewic
Time: MW 3 - 4:30
Location: Towne 313

Overview

Concurrent computation is a fundamental part of modern computer systems. However, despite the widespread use of both multithreaded and distributed programs, reasoning about the synchronization and interprocess communication behavior of concurrent systems is challenging.

The π-calculus is a minimal programming language designed for studying key features of concurrent systems, including synchronization and message passing. This course uses the π-calculus as a vehicle for studying the theoretical foundations of concurrent systems and languages for concurrent programs. It will focus on various definitions of equivalence for concurrent programs and related proof techniques such as bisimulation. As time permits, the latter part of the course will explore type systems for process calculi and the current research on designing programming languages that make it easier to reason about process behavior, for instance to rule out dead lock.

Syllabus:

1. Calculus of Communicating Systems (CCS)
   - labeled transition systems
   - strong bisimulation
   - observational/contextual equivalence
2. (Untyped) π-calculus
   - syntax
   - operational semantics
   - barbed congruence
   - may/must testing
3. Bisimilarity
   - strong & weak bisimilarity
   - up-to techniques
   - open bisimilarity
   - asynchronous variants
4. Type Systems for π-calculi
   - foundations, channel types
   - i/o types
   - linearity
   - polymorphism
   - behavioral type systems
   - lambda calculus and full abstraction

Required Texts:

• Communicating and Mobile Systems: The π-Calculus, Robin Milner
• The π-Calculus: A Theory of Mobile Processes, Davide Sangiorgi and David Walker

Other Resources:

• Calculi for Mobile Processes
• Hoare's book Communicating Sequential Processes
• CSP Archive

Last modified: 01/12/2004 11:29 AM