Parameterised Multiparty Session Types

For many application-level distributed protocols and parallel algorithms, theset of participants, the number of messages or the interaction structure areonly known at run-time. This paper proposes a dependent type theory formultiparty sessions which can statically guarantee type-safe, deadlock-freemultiparty interactions among processes whose specifications are parameterisedby indices. We use the primitive recursion operator from G\"odel's System T toexpress a wide range of communication patterns while keeping type checkingdecidable. To type individual distributed processes, a parameterised globaltype is projected onto a generic generator which represents a class of allpossible end-point types. We prove the termination of the type-checkingalgorithm in the full system with both multiparty session types and recursivetypes. We illustrate our type theory through non-trivial programming andverification examples taken from parallel algorithms and Web services usecases.Comment: LMCS 201