Session Types = Intersection Types + Union Types

Luca Padovani
(Dipartimento di Informatica, Università di Torino, Italy)

We propose a semantically grounded theory of session types which relies on intersection and union types. We argue that intersection and union types are natural candidates for modeling branching points in session types and we show that the resulting theory overcomes some important defects of related behavioral theories. In particular, intersections and unions provide a native solution to the problem of computing joins and meets of session types. Also, the subtyping relation turns out to be a pre-congruence, while this is not always the case in related behavioral theories.

In Elaine Pimentel, Betti Venneri and Joe Wells: Proceedings Fifth Workshop on Intersection Types and Related Systems (ITRS 2010), Edinburgh, U.K., 9th July 2010, Electronic Proceedings in Theoretical Computer Science 45, pp. 71–89.
Published: 21st January 2011.

ArXived at: http://dx.doi.org/10.4204/EPTCS.45.6 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org