Multiparty Symmetric Sum Types
Lasse Nielsen (DIKU, University of Copenhagen), Nobuko Yoshida, (Imperial College London), Kohei Honda (Queen Mary, University of London)

TL;DR
This paper develops a new theory of symmetric sum types for multiparty session types, enabling the modeling of non-deterministic, agreement-based choices among multiple participants, with applications in healthcare workflows.
Contribution
It introduces symmetric sum types for multiparty session types, allowing for non-deterministic, collaborative decision-making in protocols, and provides an embedding into existing types with proven properties.
Findings
Preserves typability and semantic correctness
Enables automatic translation and type checking of clinical guidelines
Supports efficient implementation of healthcare workflow tools
Abstract
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
