In modelling distributed systems where processes interact by means of message passing, one soon realises that many interactions are meant to occur following disciplined protocols.
The ability to describe complex interaction protocols by means of a formal, simple and yet expressive type language can have a profound impact on the way distributed systems are designed and developed. This is witnessed by the fact that some important standardisation bodies for web-based business and finance protocols have recently investigated design and implementation frameworks for specifying message exchange rules and validating business logic based on the notion of sessions, where session types are “shared agreements” between teams of programmers developing possibly large and complex distributed protocols or software systems.
Aim of this course is to provide a gentle introduction to session type theory, enlightening aspects which are at the core of the current research in this subject.
The course material is available at http://www.di.unito.it/~dezani/papers/ohrid.pdf.