Manifestly Phased Communication via Shared Session Types
Chuta Sano, Stephanie Balzer, and Frank Pfenning

TL;DR
This paper extends session types to shared channels with multiple clients, enabling static verification of multi-phase protocols in concurrent systems, which was not possible with prior linear session type models.
Contribution
It introduces a novel subtyping framework for shared session types, capturing multi-phase interaction protocols with manifest phases in client types.
Findings
Supports multi-phase client-server interactions
Enables static protocol verification for shared channels
Generalizes previous linear session type subtyping
Abstract
Session types denote message protocols between concurrent processes, allowing a type-safe expression of inter-process communication. Although previous work demonstrate a well-defined notion of subtyping where processes have different perceptions of the protocol, these formulations were limited to linear session types where each channel of communication has a unique provider and client. In this paper, we extend subtyping to shared session types where channels can now have multiple clients instead of a single client. We demonstrate that this generalization can statically capture protocol requirements that span multiple phases of interactions of a client with a shared service provider, something not possible in prior proposals. Moreover, the phases are manifest in the type of the client.
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.
Taxonomy
TopicsDistributed systems and fault tolerance · Logic, programming, and type systems · Formal Methods in Verification
