FOSSACS'10, joint work with Nobuko Yoshida.
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 Godel'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.
This short version is close to the paper that is publised at ETAPS 2010 [pdf].
The full version includes the full definitions, more reasoning for the examples, and proofs. This version also includes more explanations for the FFT [pdf].
The slides from the CONCUR presentation in Paris [pdf].