Session Types and Distributed Computing

Abstract

Session types offer type-based structuring principles for distributed communicating processes. They were born from process encodings of various data structures in an asynchronous version of the π-calculus. Its theory is supported and enriched by several foundations, including Linear Logic, automata theory, typed π-calculi and typed λ-calculi. Unlike types for sequential computing, where types abstract and specify data and functions, session types abstract and specify structures of interactions in sessions – they describe protocols with which processes interact with each other in possibly interleaved sessions. In this type abstraction, the division of interactions into sessions is important, classifying each set of related interactions into a distinct session, an idea which has been known and practiced in networking research since early days. This division enables tractable type abstraction, making it easy to specify protocols and to validate programs against them, statically and at runtime.

In this talk we introduce central ideas of session types through illustrative examples, identify different properties of concurrent and distributed systems which session types and associated theories can specify and guarantee, present several key technical results underpinning theories and applications of session types, and discuss open research topics. If time remains, we shall report our recent experience of the use of session types for building and verifying large-scale distributed systems.