Parameterised multiparty session types

Nobuko Yoshida; Pierre Malo Deniélou; Andi Bejleri; Raymond Hu

doi:10.1007/978-3-642-12032-9_10

Parameterised multiparty session types

Nobuko Yoshida, Pierre Malo Deniélou, Andi Bejleri, Raymond Hu

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

40 Citations (Scopus)

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ödel's System 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.

Original language	English
Title of host publication	Foundations of Software Science and Computational Structures - 13th Int. Conference, FoSSaCS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Proc.
Pages	128-145
Number of pages	18
DOIs	https://doi.org/10.1007/978-3-642-12032-9_10
Publication status	Published - 30 Apr 2010
Event	13th International Conference on the Foundations of Software Science and Computational Structures, FoSSaCS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010 - Paphos, Cyprus Duration: 20 Mar 2010 → 28 Mar 2010

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	6014 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	13th International Conference on the Foundations of Software Science and Computational Structures, FoSSaCS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010
Country/Territory	Cyprus
City	Paphos
Period	20/03/10 → 28/03/10

Access to Document

10.1007/978-3-642-12032-9_10

Cite this

Yoshida, N., Deniélou, P. M., Bejleri, A., & Hu, R. (2010). Parameterised multiparty session types. In Foundations of Software Science and Computational Structures - 13th Int. Conference, FoSSaCS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Proc. (pp. 128-145). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6014 LNCS). https://doi.org/10.1007/978-3-642-12032-9_10

Yoshida, Nobuko ; Deniélou, Pierre Malo ; Bejleri, Andi et al. / Parameterised multiparty session types. Foundations of Software Science and Computational Structures - 13th Int. Conference, FoSSaCS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Proc.. 2010. pp. 128-145 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{d2f73e75ac564bd8886913971e2de3bc,

title = "Parameterised multiparty session types",

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's System 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.",

author = "Nobuko Yoshida and Deni{\'e}lou, {Pierre Malo} and Andi Bejleri and Raymond Hu",

year = "2010",

month = apr,

day = "30",

doi = "10.1007/978-3-642-12032-9_10",

language = "English",

isbn = "3642120318",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "128--145",

booktitle = "Foundations of Software Science and Computational Structures - 13th Int. Conference, FoSSaCS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Proc.",

note = "13th International Conference on the Foundations of Software Science and Computational Structures, FoSSaCS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010 ; Conference date: 20-03-2010 Through 28-03-2010",

}

Yoshida, N, Deniélou, PM, Bejleri, A & Hu, R 2010, Parameterised multiparty session types. in Foundations of Software Science and Computational Structures - 13th Int. Conference, FoSSaCS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Proc.. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 6014 LNCS, pp. 128-145, 13th International Conference on the Foundations of Software Science and Computational Structures, FoSSaCS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Paphos, Cyprus, 20/03/10. https://doi.org/10.1007/978-3-642-12032-9_10

Parameterised multiparty session types. / Yoshida, Nobuko; Deniélou, Pierre Malo; Bejleri, Andi et al.
Foundations of Software Science and Computational Structures - 13th Int. Conference, FoSSaCS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Proc.. 2010. p. 128-145 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6014 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Parameterised multiparty session types

AU - Yoshida, Nobuko

AU - Deniélou, Pierre Malo

AU - Bejleri, Andi

AU - Hu, Raymond

PY - 2010/4/30

Y1 - 2010/4/30

N2 - 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ödel's System 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.

AB - 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ödel's System 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.

UR - http://www.scopus.com/inward/record.url?scp=77951480066&partnerID=8YFLogxK

U2 - 10.1007/978-3-642-12032-9_10

DO - 10.1007/978-3-642-12032-9_10

M3 - Conference contribution

AN - SCOPUS:77951480066

SN - 3642120318

SN - 9783642120312

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 128

EP - 145

BT - Foundations of Software Science and Computational Structures - 13th Int. Conference, FoSSaCS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Proc.

T2 - 13th International Conference on the Foundations of Software Science and Computational Structures, FoSSaCS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010

Y2 - 20 March 2010 through 28 March 2010

ER -

Yoshida N, Deniélou PM, Bejleri A, Hu R. Parameterised multiparty session types. In Foundations of Software Science and Computational Structures - 13th Int. Conference, FoSSaCS 2010, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2010, Proc.. 2010. p. 128-145. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-642-12032-9_10

Parameterised multiparty session types

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this