@article {RN58,
	title = {Parameterised Multiparty Session Types},
	journal = {Logical Methods in Computer Science},
	volume = {8},
	number = {4},
	year = {2012},
	type = {Journal Article},
	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 G{\"o}del{\textquoteright}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.

},
	keywords = {Computer Science, D.1.3, F.1.1, F.1.2, F.3.3, Logic in Computer Science},
	issn = {1860-5974},
	doi = {10.2168/Lmcs-8(4:6)2012},
	url = {<Go to ISI>://WOS:000315381600008},
	author = {Denielou, P. M. and Yoshida, N. and Bejleri, A. and Hu, R.}
}
