A Gentle Introduction to Session Types

Abstract

We present session types, a type formalism for structured communication. The goal of the thesis is to give an elementary introduction to session types for a new reader with only a little or no knowledge of related concepts, such as π-calculus or type systems. We start by motivating the reader with an informal example and later define the language formally. Only basic language constructs are defined at the beginning and the language is extended gradually. We prove the soundness of the type system, give practical example how session types help developing server- client systems and finally talk briefly about extensions and related work.