Thursdays, 10-12
Room: 3A18
Starting 8th February

PhD course, 2.5 ECTS
Exam: paper presentation in the second part of the course

Contact: Agata Murawska (
We also have a mailing list,, which can be joined here

Feb. 8 Calculus of Communicating Systems
Syntax, semantics, limitations
Based on: R. Milner, "Communication and Concurrency"

Feb. 15 Calculus of Communicating Systems
Reduction semantics, trace equivalence, bisimulation and bisimilarity, weak bisimulation and weak bisimilarity
Based on: R. Milner, "Communication and Concurrency"

Feb. 22 Pi Calculus
Based on: J. Parrow, "An introduction to the pi-calculus" (available online)

Mar. 1 True concurrency
Mar. 8 Expressivity
Mar. 15 Psi calculi
Mar 22 Session Types
Mar 29 ( Easter Break )

Course description
The course will focus on concurrency theory and its applications. The first part of the course will consist of 8-10 lectures given by experts in the field, and providing an in-depth introduction to the topic. The program for this part will include the following topics:
  1. Calculus of Communicating Systems
  2. Different kinds of semantics
  3. Synchronous (and asynchronous) Pi calculus
  4. Observable behaviours and bisimulation
  5. Session types and multi-party session types
  6. Expressivity
  7. Connection to linear logic
  8. Choreographies

In the second part, the focus will be put on recent results in concurrency theory. With a solid background provided in the first part, a number of influential papers from the last few years will be discussed in depth. The precise selection will be based on the research interests of the participants.

Reading list (for the first part of the course) includes:

  • R. Milner; Communicating and Mobile Systems: the pi-Calculus
  • R. Milner; Communication and Concurrency
  • D. Sangiorgi, D. Walker; The pi-calculus: a Theory of Mobile Processes
  • S. Gay, A. Ravara; Behavioural Types: From Theory to Tools
  • R. Milner; The Space and Motion of Communicating Agents

  • D. Gorla; Towards a Unified Approach to Encodability and Separation Results for Process Calculi
  • K. Takeuchi, K.Honda, M. Kubo; An interaction-based language and its typing system
  • K. Honda, N. Yoshida, M. Carbone; Multiparty Asynchronous Session Types
  • L. Caires, F. Pfenning; Session Types as Intuitionistic Linear Propositions
  • P. Wadler; Propositions as Sessions

PhD dissertation
  • F. Montesi; Choreographic Programming