Session Types for Broadcasting
Dimitrios Kouzapas (University of Glasgow), Ram\=unas Gutkovas, (Uppsala University), Simon J. Gay (University of Glasgow)

TL;DR
This paper introduces a novel session type theory tailored for broadcast communication, relaxing traditional assumptions of point-to-point and reliable communication, and leveraging the broadcasting psi-calculi framework for enhanced understanding.
Contribution
It develops a session type framework for broadcast semantics that does not assume point-to-point or reliable communication, extending session types to more general communication models.
Findings
The framework is sound and safe.
Provides insights into session types in broadcast settings.
Lays groundwork for broader application of session types.
Abstract
Up to now session types have been used under the assumptions of point to point communication, to ensure the linearity of session endpoints, and reliable communication, to ensure send/receive duality. In this paper we define a session type theory for broadcast communication semantics that by definition do not assume point to point and reliable communication. Our session framework lies on top of the parametric framework of broadcasting psi-calculi, giving insights on developing session types within a parametric framework. Our session type theory enjoys the properties of soundness and safety. We further believe that the solutions proposed will eventually provide a deeper understanding of how session types principles should be applied in the general case of communication semantics.
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.
