Session Types

Session types are a type-theoretic framework for specifying and enforcing communication protocols in concurrent and distributed systems. Originating in the 1990s through the work of Kohei Honda and later developed by Simon Gay and Antonio Ravara, session types treat communication channels as typed objects: a channel's type describes not merely the kind of data transmitted, but the exact sequence of messages, their directions (send or receive), and the resulting channel state after each exchange. A well-typed program in a session-typed language is guaranteed to be free of certain classes of communication errors — mismatched message types, deadlocks from incomplete protocols, and race conditions from conflicting channel uses.

The connection to linear logic is direct and productive. Session types are the computational manifestation of linear logic's resource-sensitive propositions: a channel of session type S is a resource that must be used exactly once according to the protocol S. The multiplicative conjunction of linear logic corresponds to the parallel composition of sessions; the linear implication corresponds to the delegation of a session from one process to another. This correspondence has been made precise through Curry-Howard interpretations that map session-typed process calculi directly into linear logic proof systems, and vice versa.

Session types have been extended to handle multiparty protocols (where more than two agents interact), gradual typing (which mixes static and dynamic session checking), and dependent session types (where the type of a message can depend on the value of a previous message). These extensions bring session types closer to the expressiveness needed for real-world distributed systems, where protocols are rarely binary, rarely fully static, and often involve value-dependent behavior.

Session types represent a rare convergence of practical software engineering and deep theoretical structure. Most type systems for concurrency are either theoretically elegant but practically unusable, or practically useful but theoretically ad hoc. Session types are both — and the reason is that they are not a clever invention of computer scientists but a discovery: the communication protocols that programmers write by hand are already structured like linear logic proofs, and the type system merely makes this structure explicit. The implication is unsettling: if communication protocols are proofs, then protocol violations are not merely bugs but logical errors — failures of reasoning, not failures of implementation.