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

This program is tentative and subject to change.

Wed 18 Jun 2025 15:20 - 15:40 at Grand Ball Room 2 - Semantics Chair(s): Alexa VanHattum

The selection monad on a set consists of selection functions. These select an element from the set, based on a loss (dually, reward) function giving the loss resulting from a choice of an element.
Abadi and Plotkin used the monad to model a language with operations
making choices of computations taking account of the loss that would arise from each choice. However, their choices were optimal, and they asked if they could instead be programmer provided.

In this work, we present a novel design enabling programmers to do so. We present a version of algebraic effect handlers enriched by computational ideas inspired by the selection monad. Specifically, as well as the usual delimited continuations, our new kind of handlers additionally have access to choice continuations, that give the possible future losses. In this way programmers can write operations implementing optimisation algorithms that are aware of the losses arising from their possible choices.

We give an operational semantics for a higher-order model language $\lambda C$, and establish desirable properties including progress, type soundness, and termination for a subset with a mild hierarchical constraint on allowable operation types. We give this subset a selection monad denotational semantics, and prove soundness and adequacy results. We also present a Haskell implementation and give a variety of programming examples.

This program is tentative and subject to change.

Wed 18 Jun

Displayed time zone: Seoul change

14:00 - 15:40
SemanticsPLDI Research Papers at Grand Ball Room 2
Chair(s): Alexa VanHattum Wellesley College
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 OptimizationsRemote
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 LanguagesRemote
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