SPLASH 2026
Sun 4 - Fri 9 October 2026 Oakland, California, United States
co-located with SPLASH/ISSTA 2026
Tue 6 Oct 2026 14:06 - 14:24 at Junior Ballroom 1&2 - Session Types and Concurrency Chair(s): Peter Thiemann

\emph{Multiparty session types} (MPST) are a type discipline for
concurrent and distributed systems, designed to ensure not only type
safety and deadlock-freedom, but also \emph{liveness} of typed
communicating processes. Two main MPST methodologies, top-down and
bottom-up, have been proposed and are integrated into a wide range of
programming languages and tools. The \emph{top-down} strategy starts
by specifying the overall choreography of the protocol (called a
global type), from which a set of local types that satisfy safety and
liveness are generated by endpoint projection (EPP). Once each
participant is type-checked against a generated local type, liveness
of the set of typed processes is automatically ensured \emph{by
construction}. The \emph{bottom-up} strategy directly checks whether
local types inferred from processes satisfy liveness in order to
enforce liveness of processes. Since the top-down strategy depends on
global types and the EPP algorithms, it has often been considered that
the top-down system offers \emph{strictly less typability} than the
bottom-up system. Our paper negates this belief. We prove that, using
the precise subtyping for the subsumption rule, the top-down strategy
offers \emph{exactly the same typability} as the bottom-up system.
More precisely, a multiparty session $M$ is typable and verified to be
live by the bottom-up typing system if and only if $M$ is typable by
the top-down typing system. The key to the proof is the development
of a \emph{principal global type inference algorithm} which builds a
\emph{principal} global type from an arbitrary set of live local
types. We have implemented the global type inference algorithm
together with projection, process type checking and local type
inference algorithms, and built a toolchain for both the top-down and
bottom-up strategies. We evaluated our toolchain with representative
examples from the literature, confirming that the top-down approach is
more efficient than the bottom-up approach.

Tue 6 Oct

Displayed time zone: Pacific Time (US & Canada) change

13:30 - 15:00
Session Types and ConcurrencyOOPSLA at Junior Ballroom 1&2
Chair(s): Peter Thiemann University of Freiburg
13:30
18m
Talk
Speak Now: Safe Actor Programming with Multiparty Session Types
OOPSLA
Simon Fowler University of Glasgow, Raymond Hu Queen Mary University of London
DOI
13:48
18m
Talk
Mixed Choice in Asynchronous Multiparty Session Types
OOPSLA
Laura Bocchi University of Kent, Raymond Hu Queen Mary University of London, Adriana Laura Voinea University of Glasgow, Simon Thompson University of Kent
DOI
14:06
18m
Talk
Top-Down = Bottom-Up: Sound and Complete Characterisations of Liveness by Multiparty Global Protocols
OOPSLA
Kai Pischke University of Oxford, Nobuko Yoshida University of Oxford
DOI
14:24
18m
Talk
A Design Space Exploration of Async/Await
OOPSLA
Gavin Gray Brown University, Shriram Krishnamurthi Brown University, Will Crichton Brown University
DOI Pre-print