Sciweavers

FOSSACS
2010
Springer

Parameterised Multiparty Session Types

13 years 10 months ago
Parameterised Multiparty Session Types
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¨odel’s System T to express a wide range of communication patterns while keeping type checking decidable. We illustrate our type theory through non-trivial programming and verification examples taken from parallel algorithms and Web services usecases.
Nobuko Yoshida, Pierre-Malo Deniélou, Andi
Added 18 May 2010
Updated 18 May 2010
Type Conference
Year 2010
Where FOSSACS
Authors Nobuko Yoshida, Pierre-Malo Deniélou, Andi Bejleri, Raymond Hu
Comments (0)