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

This program is tentative and subject to change.

Wed 22 Jan 2025 15:40 - 16:00 at Marco Polo - Probabilistic Programming 1

Imprecise probability is concerned with uncertainty about which probability distributions to use. It has applications in robust statistics and machine learning.

We look at programming language models for imprecise probability. Our desiderata are that we would like our model to support all kinds of composition, categorical and monoidal; in other words, guided by dataflow diagrams. Another equivalent perspective is that we would like a model of synthetic probability in the sense of Markov categories.

Imprecise probability can be modelled in various ways, with the leading monad-based approach using convex sets of probability distributions. This model is not fully compositional because the monad involved is not commutative, meaning it does not have a proper monoidal structure. In this work, we provide a new fully compositional account. The key idea is to name the non-deterministic choices. To manage the renamings and disjointness of names, we use graded monads. We show that the resulting compositional model is maximal and relate it with the earlier monadic approach, proving that we obtain tighter bounds on the uncertainty.

This program is tentative and subject to change.

Wed 22 Jan

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

15:00 - 16:20
Probabilistic Programming 1POPL at Marco Polo
15:00
20m
Talk
A quantitative probabilistic relational Hoare logic
POPL
Martin Avanzini Inria, Gilles Barthe MPI-SP; IMDEA Software Institute, Benjamin Gregoire INRIA, Davide Davoli Université Côte d’Azur, Inria
15:20
20m
Talk
Approximate Relational Reasoning for Higher-Order Probabilistic Programs
POPL
Philipp G. Haselwarter Aarhus University, Kwing Hei Li Aarhus University, Alejandro Aguirre Aarhus University, Simon Oddershede Gregersen New York University, Joseph Tassarotti New York University, Lars Birkedal Aarhus University
Pre-print
15:40
20m
Talk
Compositional imprecise probability: a solution from graded monads and Markov categories
POPL
Jack Liell-Cock University of Oxford, Sam Staton University of Oxford
16:00
20m
Talk
Sound and Complete Proof Rules for Probabilistic Termination
POPL