TY - JOUR T1 - Parameterised Multiparty Session Types JF - Logical Methods in Computer Science Y1 - 2012 A1 - Denielou, P. M. A1 - Yoshida, N. A1 - Bejleri, A. A1 - Hu, R. KW - Computer Science KW - D.1.3 KW - F.1.1 KW - F.1.2 KW - F.3.3 KW - Logic in Computer Science AB - 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. VL - 8 UR - ://WOS:000315381600008 U1 - Cyberinfrastructure U2 - ER -