Session Types = Intersection Types + Union Types

TL;DR

This paper introduces a new semantic framework for session types using intersection and union types, addressing key limitations of existing behavioral theories and improving type operations and subtyping properties.

Contribution

It develops a novel theory of session types based on intersection and union types, providing natural modeling of branching and better type operations.

Findings

Intersection and union types model branching points effectively.

The theory solves join and meet computations for session types.

Subtyping becomes a pre-congruence in this framework.

Abstract

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.