Abstract: In complex distributed systems, communicating participants agree on a protocol to follow, by specifying the type and direction of data exchanged. Session types are an elegant type formalism used to model structured communication-based programming. They guarantee privacy, communication safety and session fidelity. A binary session type describes communication among two participants, as opposed to multiparty session type, which describes communication among two or more participants.
In these lectures we will focus mainly on binary session types and the pi-calculus, a core communication and concurrency calculus, which is the original and most successful framework for session types. We will give the statics and dynamics of the language and illustrate these with several examples and exercises. We will present some advanced topics on session types as well as their logical foundations. Finally, we will present how session types are integrated in mainstream programming languages, with main focus on Java, and a summary of session-based software tools for specifying and verifying communicating protocols in distributed scenarios.

The content in these slides was presented during the BehAPI 2019 Summer School in Leicester.