Foundation of Session Types

International audienceSessions are a common and widespread mechanism of interaction in distributed architectures. Two processes wanting to interact establish a connection on a common public channel. In this connection they agree on some private channel on which to have a conversation, dubbed session. The conversation follows a given protocol which describes the kind and order of the messages exchanged on the private channel. In general, a protocol does not specify a unique sequence of interactions. At any point of the interaction the rest of the conversation for a partner may vary according to its own or its partner's choices which complicates formal specification of protocols. Session types are a solution proposed to specify session protocols. They describe the sequences of messages exchanged on a private session channel and their possible branching. Many (substantially different) variants of session types have been put forward. They vary according to the programming language they target, the type containment relations and the specific features they aim to capture. In this work we present a basic and unified foundation of session types that is as much language independent as possible. All session types proposed in the literature (with the exception of the polymorphic ones) are particular cases of the session types discussed here. In fact we present a streamlined theory of session types based on a simple yet general and expressive formalism whose main features are semantically characterised and where each design choice is semantically justified. We formally define the semantics of session types and use it to define the subsessioning relation. We give a coinductive characterization of subsessioning and describe algorithms to decide all the key relations defined in the article