MobilityReadingGroup

Parameterised Multiparty Session Types

Pierre-Malo DENIÉLOU, Nobuko YOSHIDA, Andi BEJLERI, Raymond HU

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.

@article{DYBH2012,
  author = {Pierre-Malo Deniélou and Nobuko Yoshida and Andi Bejleri and Raymond Hu},
  title = {{Parameterised Multiparty Session Types}},
  journal = {LMCS},
  volume = {8},
  issue = {4},
  pages = {--},
  year = 2012
}

@article{DYBH2012,
  author = {Pierre-Malo Deniélou and Nobuko Yoshida and Andi Bejleri and Raymond Hu},
  title = {{Parameterised Multiparty Session Types}},
  journal = {Logical Methods in Computer Science},
  volume = {8},
  issue = {4},
  pages = {--},
  doi = "10.2168/LMCS-8(4:6)2012",
  year = 2012
}