POPL 2025
Sun 19 - Sat 25 January 2025 Denver, Colorado, United States

This program is tentative and subject to change.

Fri 24 Jan 2025 15:20 - 15:40 at Marco Polo - Concurrency 2

Multiparty session types (MPST) provide a type discipline for ensuring communication safety, deadlock-freedom and liveness for multiple concurrently running participants. The original formulation of MPST takes the \emph{top-down} approach, where a \emph{global type} specifies a bird’s eye view of the intended interactions between participants, and each distributed process is locally type-checked against its end-point projection. A more recent one takes the \emph{bottom-up} approach, where a desired property $\varphi$ of a set of participants is ensured if the same property $\varphi$ is true for an ensemble of end-point types (a typing context) inferred from each participant.

This paper compares these two main procedures of MPST, giving their detailed complexity analyses. To this aim, we build several new algorithms missing from the bottom-up or top-down workflows by using graph representation of session types (\emph{type graphs}). We first propose a subtyping system based on type graphs, offering more efficient (quadratic) subtype-checking than the existing (exponential) inductive algorithm. Next for the top-down, we measure complexity of the four end-point projections from the literature. For the coinductive projection, we build a new sound and complete algorithm using type graphs. For bottom-up, we develop a novel \emph{type inference system} from MPST processes which generates \emph{minimum type graphs}, succinctly capturing covariance of internal choice and contravariance of external choice. For property-checking of typing contexts, we achieve PSPACE-hardness by reducing it from the quantified Boolean formula (QBF) problem, and build nondeterministic algorithms that search for counterexamples to prove membership in PSPACE. We also present deterministic analogues of these algorithms that run in exponential time. Finally, we calculate the total complexity of the top-down and the bottom-up approaches. Our analyses reveal that the top-down based on global types is more efficient than the bottom-up in many realistic cases; liveness checking for typing contexts in the bottom-up has the highest complexity; and the type inference costs exponential against the size of a process, which impacts the total complexity.

This program is tentative and subject to change.

Fri 24 Jan

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

15:00 - 16:20
Concurrency 2POPL at Marco Polo
15:00
20m
Talk
Flo: a Semantic Foundation for Progressive Stream Processing
POPL
Shadaj Laddad University of California at Berkeley, Alvin Cheung University of California at Berkeley, Joseph M. Hellerstein UC Berkeley, Mae Milano Princeton University
Pre-print
15:20
20m
Talk
Top-Down or Bottom-Up? Complexity Analyses of Synchronous Multiparty Session Types
POPL
Thien Udomsrirungruang University of Oxford, Nobuko Yoshida University of Oxford
15:40
20m
Talk
Semantic Logical Relations for Timed Message-Passing Protocols
POPL
Yue Yao Carnegie Mellon University, Grant Iraci University at Buffalo, Cheng-En Chuang University at Buffalo, Stephanie Balzer Carnegie Mellon University, Lukasz Ziarek University at Buffalo
16:00
20m
Talk
Reachability Analysis of the Domain Name System
POPL
Dhruv Nevatia ETH Zurich, Si Liu ETH Zurich, David Basin ETH Zurich