Multiparty Symmetric Sum Types
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 determini...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2010-11-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1011.6436v1 |
| _version_ | 1824019419001520128 |
|---|---|
| author | Lasse Nielsen Nobuko Yoshida Kohei Honda |
| author_facet | Lasse Nielsen Nobuko Yoshida Kohei Honda |
| author_sort | Lasse Nielsen |
| collection | DOAJ |
| description | 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 using 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. |
| first_indexed | 2024-12-19T01:19:08Z |
| format | Article |
| id | doaj.art-2cebf62162284eb4a34878eff8d360b5 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-19T01:19:08Z |
| publishDate | 2010-11-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-2cebf62162284eb4a34878eff8d360b52022-12-21T20:42:32ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802010-11-0141Proc. EXPRESS 201012113510.4204/EPTCS.41.9Multiparty Symmetric Sum TypesLasse NielsenNobuko YoshidaKohei HondaThis 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 using 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.http://arxiv.org/pdf/1011.6436v1 |
| spellingShingle | Lasse Nielsen Nobuko Yoshida Kohei Honda Multiparty Symmetric Sum Types Electronic Proceedings in Theoretical Computer Science |
| title | Multiparty Symmetric Sum Types |
| title_full | Multiparty Symmetric Sum Types |
| title_fullStr | Multiparty Symmetric Sum Types |
| title_full_unstemmed | Multiparty Symmetric Sum Types |
| title_short | Multiparty Symmetric Sum Types |
| title_sort | multiparty symmetric sum types |
| url | http://arxiv.org/pdf/1011.6436v1 |
| work_keys_str_mv | AT lassenielsen multipartysymmetricsumtypes AT nobukoyoshida multipartysymmetricsumtypes AT koheihonda multipartysymmetricsumtypes |