Computing Publications

Publications Home » Parameterised Multiparty Session Types

Parameterised Multiparty Session Types

Andi Bejleri, Pierre-Malo , Raymond Hu, Nobuko Yoshida

Conference or Workshop Paper
International Conference on Foundations of Software Science and Computation Structures
March, 2010
Lecture Notes in Computer Science
Volume 6014
Issue 2010
pp.128–145
Springer-Verlag
ISBN 978-3-642-12031-2
ISSN 0302-9743
DOI 10.1007/978-3-642-12032-9
Abstract

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.

Keywords
Concurrency
Process Calculi
Session Types
SLURP
Theory of Computational Systems
PDF of full publication (287 kilobytes)
(need help viewing PDF files?)
BibTEX file for the publication
N.B.
Conditions for downloading publications from this site.
 

pubs.doc.ic.ac.uk: built & maintained by Ashok Argent-Katwala.