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

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


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.


  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:

Other Resources:

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