Session Types for Broadcasting

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.