Semantic subtyping for session types

Semantic subtyping consists of defining a set-theoretic model of types and stating that one type is subtype of another one if the interpretation of the former is a subset of the interpretation of the latter. The semantic approach to subtyping for session types entails some intrinsic technical difficulties, but it highlights fundamental (and often understated) properties of sessions. As a concrete example, we show that the standard, syntactically-defined subtyping for dyadic session types does not scale well to multi-party sessions. We semantically define a subtyping relation for multi-party session types and show how it relates with the standard one.