Pierre-Malo Denielou ; Nobuko Yoshida ; Andi Bejleri ; Raymond Hu - Parameterised Multiparty Session Types

lmcs:924 - Logical Methods in Computer Science, October 11, 2012, Volume 8, Issue 4 - https://doi.org/10.2168/LMCS-8(4:6)2012
Parameterised Multiparty Session Types

Authors: Pierre-Malo Denielou ; Nobuko Yoshida ORCID-iD; Andi Bejleri ; Raymond Hu ORCID-iD

    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.


    Volume: Volume 8, Issue 4
    Published on: October 11, 2012
    Accepted on: June 25, 2015
    Submitted on: January 14, 2011
    Keywords: Computer Science - Logic in Computer Science,F.3.3, D.1.3, F.1.1, F.1.2
    Fundings :
      Source : OpenAIRE Research Graph
    • Multiparty Session Types: Theory and Conversation-Oriented Programming; Funder: UK Research and Innovation; Code: EP/G015635/1
    • Engineering Foundations of Web Services: Theories and Tool Support; Funder: UK Research and Innovation; Code: EP/F003757/1

    Linked data

    Source : ScholeXplorer IsCitedBy DOI 10.4230/lipics.concur.2020.12
    • 10.4230/lipics.concur.2020.12
    Session Subtyping and Multiparty Compatibility Using Circular Sequents
    Horne, Ross James ;

    34 Documents citing this article

    Share

    Consultation statistics

    This page has been seen 732 times.
    This article's PDF has been downloaded 416 times.