Fundamentals of session types

We present a reconstruction of session types in a linear pi calculus where types are qualified as linear or unrestricted. Linearly qualified communication channels are guaranteed to occur in exactly one thread, possibly multiple times; unrestricted (or shared) channels may appear in an unbounded number of threads. In our language each channel is characterized by two distinct variables, one used for reading, the other for writing; scope restriction binds together two variables, thus establishing the correspondence between the two ends of the same channel. This mechanism allows a precise control of resources via a conventional linear type system. Furthermore, the uniform treatment of linear and shared channels leads to a surprisingly simply theory which, in addition, extends typability when compared to traditional systems for session types. We build the language gradually, starting from simple input/output, then adding recursive types, replication and finally choice. We also present an algorithmic type checking system.