Multiparty symmetric sum types
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Standard
Multiparty symmetric sum types. / Nielsen, Lasse; Yoshida, Nobuko; Honda, Kohei.
Proceedings 17th International Workshop on Expressiveness in Concurrency . ed. / Sibylle Fröschle; Frank D. Valencia. Vol. 41 2010. p. 121-135 (Electronic Proceedings in Theoretical Computer Science).Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - GEN
T1 - Multiparty symmetric sum types
AU - Nielsen, Lasse
AU - Yoshida, Nobuko
AU - Honda, Kohei
N1 - Conference code: 17
PY - 2010
Y1 - 2010
N2 - This paper introduces a new theory of multiparty session types based on symmetric sum types, by which we can type non-deterministic orchestration choice behaviours. While the original branching type in session types can represent a choice made by a single participant and accepted by others determining how the session proceeds, the symmetric sum type represents a choice made by agreement among all the participants of a session. Such behaviour can be found in many practical systems, including collaborative workflow in healthcare systems for clinical practice guidelines (CPGs).Processes with the symmetric sums can be embedded into the original branching types using conductor processes. We show that this type-driven embedding preserves typability, satisfies semantic soundness and completeness, and meets the encodability criteria adapted to the typed setting. The theory leads to an efficient implementation of a prototypical tool for CPGs which automatically translates the original CPG specifications from a representation called the Process Matrix to symmetric sum types,type checks programs and executes them.
AB - This paper introduces a new theory of multiparty session types based on symmetric sum types, by which we can type non-deterministic orchestration choice behaviours. While the original branching type in session types can represent a choice made by a single participant and accepted by others determining how the session proceeds, the symmetric sum type represents a choice made by agreement among all the participants of a session. Such behaviour can be found in many practical systems, including collaborative workflow in healthcare systems for clinical practice guidelines (CPGs).Processes with the symmetric sums can be embedded into the original branching types using conductor processes. We show that this type-driven embedding preserves typability, satisfies semantic soundness and completeness, and meets the encodability criteria adapted to the typed setting. The theory leads to an efficient implementation of a prototypical tool for CPGs which automatically translates the original CPG specifications from a representation called the Process Matrix to symmetric sum types,type checks programs and executes them.
KW - Faculty of Science
KW - computer science
KW - multiparty
KW - session types
KW - interaction
KW - communication
KW - decission
KW - sum types
U2 - 10.4204/EPTCS.41.9
DO - 10.4204/EPTCS.41.9
M3 - Article in proceedings
VL - 41
T3 - Electronic Proceedings in Theoretical Computer Science
SP - 121
EP - 135
BT - Proceedings 17th International Workshop on Expressiveness in Concurrency
A2 - Fröschle, Sibylle
A2 - Valencia, Frank D.
T2 - 17th International Workshop on Expressiveness in Concurrency
Y2 - 30 August 2010 through 30 August 2010
ER -
ID: 172644242