POPL'11, joint work with Nobuko Yoshida.
Multiparty session types enforce structured safe communications between several participants, as long as their number is fixed when the session starts. In order to handle common distributed interaction patterns such as cloud algorithms or peer-to-peer protocols, we propose a new role-based multiparty session type theory where roles are defined as classes of local behaviours that an arbitrary number of participants can dynamically join and leave. We offer programmers a polling operation that gives access to the current set of a role's participants in order to fork processes. Our type system with universal types for polling can handle this dynamism and retain type safety. A multiparty locking mechanism is introduced to provide communication safety, but also to ensure a stronger progress property for joining participants that has never been guaranteed in previous systems. Finally, we present some implementation mechanisms used in our prototype extension of ML.
This short version is quite similar to the one that appeared in the proceedings [pdf].
The long version provides definitions, examples and proofs [pdf].
Here is the source code of a preliminary implementation of a programming language with the semantics described in the paper [tar.gz]. It consists of the source code of the compiler (in /src), the runtime (in /lib) and the examples from the paper (in /exp). It requires make, a recent Ocaml compiler and the graph visualisation program dot. It has been tested under Linux. In the example directories, 'make' produces an implementation and a continuation-based API that the user can use.