Parameterised multiparty session types

Pierre Malo Deniélou, Nobuko Yoshida, Andi Bejleri, Raymond Hu

    Research output: Contribution to journalArticlepeer-review

    37 Citations (Scopus)


    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 parameterized 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 parameterized 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.

    Original languageEnglish
    JournalLogical Methods in Computer Science (LMCS)
    Issue number4
    Publication statusPublished - 5 Nov 2012


    • Dependent types
    • FFT
    • Gödel T
    • Parallel algorithms
    • Session types
    • The Pi-Calculus
    • Web services


    Dive into the research topics of 'Parameterised multiparty session types'. Together they form a unique fingerprint.

    Cite this