PLDI 2025
Mon 16 - Fri 20 June 2025 Seoul, South Korea

This program is tentative and subject to change.

Wed 18 Jun 2025 14:00 - 14:20 at Grand Ball Room 2 - Semantics

Nondeterminism introduced by race conditions and message reorderings makes parallel and
distributed programming hard. Nevertheless, promising approaches such as LVars and CRDTs address
this problem by introducing a partial order structure on shared state that describes how the state evolves over time. \emph{Monotone} programs that respect the order are deterministic. Datalog-inspired languages incorporate this idea of monotonicity in a first-class way but they are not general-purpose. We would like parallel and distributed languages to be as natural to use as any
functional language, without sacrificing expressivity, and with a formal basis of
study as appealing as the lambda calculus.

This paper presents $\lambda_\vee$, a core language for deterministic parallelism that embodies the ideas above. In $\lambda_\vee$, values may increase over time according to a \emph{streaming order} and all computations are monotone with respect to that order. The streaming order coincides with the approximation order found in Scott semantics and so unifies the foundations of functional programming with the foundations of deterministic distributed computation. The resulting lambda calculus has a computationally adequate model rooted in domain theory. It integrates the compositionality and power of abstraction characteristic of functional programming with the declarative nature of Datalog.

This program is tentative and subject to change.

Wed 18 Jun

Displayed time zone: Seoul change

14:00 - 15:40
14:00
20m
Talk
Functional Meaning for Parallel Streaming
PLDI Research Papers
Nick Rioux University of Pennsylvania, Steve Zdancewic University of Pennsylvania
DOI Pre-print
14:20
20m
Talk
MISAAL: Synthesis-Based Automatic Generation of Efficient and Retargetable Semantics-Driven Optimizations
PLDI Research Papers
Abdul Rafae Noor University of Illinois at Urbana-Champaign, Dhruv Baronia University of Illinois at Urbana-Champaign, Akash Kothari University of Illinois at Urbana-Champaign, Muchen Xu University of Illinois at Urbana-Champaign, Charith Mendis University of Illinois at Urbana-Champaign, Vikram S. Adve University of Illinois at Urbana-Champaign
DOI
14:40
20m
Talk
First-Class Verification Dialects for MLIR
PLDI Research Papers
Mathieu Fehr The University of Edinburgh, Yuyou Fan University of Utah, Hugo Pompougnac Université Grenoble Alpes; Inria; CNRS; Grenoble INP, John Regehr University of Utah, Tobias Grosser University of Cambridge
DOI
15:00
20m
Talk
[TOPLAS] A Modular Approach to Metatheoretic Reasoning for Extensible Languages
PLDI Research Papers
Dawn Michaelson University of Minnesota, Gopalan Nadathur University of Minnesota, Eric Van Wyk University of Minnesota - Twin Cities
15:20
20m
Talk
Handling the Selection Monad
PLDI Research Papers
Gordon Plotkin Google DeepMind, Ningning Xie University of Toronto
DOI