Session Types at the Mirror

TL;DR

This paper redefines session types as process behavior projections with a semantics based on fair testing, unifying behavioral types with features of conversation and multi-party session types, enabling semantic reasoning about their properties.

Contribution

It introduces a semantic framework for session types based on fair testing, unifying various types and providing a foundation for semantic analysis.

Findings

Unified theory of behavioral types with fair testing semantics

Encompasses dyadic and multi-party session types

Allows semantic reasoning about well-typedness and subtyping

Abstract

We (re)define session types as projections of process behaviors with respect to the communication channels they use. In this setting, we give session types a semantics based on fair testing. The outcome is a unified theory of behavioral types that shares common aspects with conversation types and that encompass features of both dyadic and multi-party session types. The point of view we provide sheds light on the nature of session types and gives us a chance to reason about them in a framework where every notion, from well-typedness to the subtyping relation between session types, is semantically -rather than syntactically- grounded.