Parameterised Multiparty Session Types

Abstract

For many application-level distributed protocols and parallel algorithms, the set of participants, the number of messages or the interaction structure are only known at run-time. This paper proposes a dependent type theory for multiparty sessions which can statically guarantee type-safe, deadlock-free multiparty interactions among processes whose specifications are parameterised by indices. We use the primitive recursion operator from Gödel's System T to express a wide range of communication patterns while keeping type checking decidable. To type individual distributed processes, a parameterised global type is projected onto a generic generator which represents a class of all possible end-point types. We prove the termination of the type-checking algorithm in the full system with both multiparty session types and recursive types. We illustrate our type theory through non-trivial programming and verification examples taken from parallel algorithms and Web services usecases.

LMCS 2012

References in corpus (1)

• Multiparty Symmetric Sum Types

Cited by in corpus (9)

• Globally Governed Session Semantics
• CAMP: Cost-Aware Multiparty Session Protocols
• Towards deductive verification of MPI programs against session types
• A Typeful Characterization of Multiparty Structured Conversations Based on Binary Sessions
• Session Types with Runtime Adaptation: Overview and Examples
• Architectures in parametric component-based systems: Qualitative and quantitative modelling
• A Session Type System for Asynchronous Unreliable Broadcast Communication
• A Theory of Available-by-Design Communicating Systems
• Modelling architectures of parametric weighted component-based systems