Parameterised Session Types Communication Patterns: Through the Looking Glass of Session Types

This dissertation studies a type theory to guarantee communication-safety in sessions of an arbitrary number of participants, typically represented as communication patterns, of mobile processes in the context of multiparty session types— a well-established type theory that describes the interactive structure of a fixed number of processes from a global point of view and type-checks the processes through projection of the global type onto the participants of the session. Communication-safety is the property that mobile processes exchange values of the same set without deadlocking and data races. Our study introduces a programming idiom of roles— a concept that describes the nature of a communication pattern in a similar way to classes in Java and C#, offering a design on how to incorporate parameterised session types into a mainstream language. The formal model (1) preserves multiparty session types’ syntax and type-checking strategy, and (2) allows the number of participants to range over infinite sets of natural numbers, providing full computation power of programs. A series of communication patterns and real-world examples from parallel algorithms and data exchange protocols demonstrate the expressiveness and practicality of the formal model, comparing the model with the only mature implementation of (binary) session types. We proved that type preservation under reduction and communication-safety hold in the type system. The study of parameterised session types is supported by the examination of multiparty session types for synchronous communications. We extended the initial work on multiparty session types with a simpler calculus, multicast send of values and labels, a practical form of higher-order communication and a more intuitive, elegant linearity property; we proved that (a) type preservation and communication-safety hold in the type system, and (b) interactions of a typeable process follow exactly the description of the global type