Protocol Specifications for Concurrent and Distributed Systems

Academic year 2023/24

Advanced course
Lecturer: Nobuko Yoshida, University of Oxford, UK
Session types are a popular approach for the verification and specification of message-passing programs. This course:

• introduces the syntax and semantics of a process calculus to formally reason about communicating programs;
• presents the binary session type system, which disciplines the communication of pairs of concurrent processes and guarantees type preservation and progress; and
• extends the binary session-type approach to systems of multiple (two or more) concurrent participants, by introducing multiparty session types.

Examples and exercises are provided, and no prior knowledge of session types is required.

References and material