Session Types for Broadcasting

Dimitrios Kouzapas
(University of Glasgow)
Ramūnas Gutkovas
(Uppsala University)
Simon J. Gay
(University of Glasgow)

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.

In Alastair F. Donaldson and Vasco T. Vasconcelos: Proceedings 7th Workshop on Programming Language Approaches to Concurrency and Communication-cEntric Software (PLACES 2014), Grenoble, France, 12 April 2014, Electronic Proceedings in Theoretical Computer Science 155, pp. 25–31.
Published: 12th June 2014.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: