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

Andi Bejleri, Imperial College London, UK

Communication patterns describe simple and elegant structured interactions in communication based applications. They are used in many parallel computing architectures of parallel algorithms, data exchange protocols and web-services. Communication patterns help programmers to design more efficient, structured, modular and understandable architectures, but they do not provide any automatic code validation.

We study this problem using global session types, a type theory that describes structured interactions from a global point of view. The calculus used in this study is a variant of the Pi-calculus extended with primitives for structuring interactions, based on the initial calculus of multiparty sessions. This calculus (language) is explained through a human analogy of an edifice with many chatting rooms. Our formal system allows programmers to represent parameterised communication patterns by global types and then validate the code by type-checking. Examples of parallel algorithms and data exchange protocol illustrate the practical utility of our system.