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:00 - 15:20 at Marco Polo - Probabilistic Programming 1

We introduce eRHL, a program logic for reasoning about relational expectation properties of pairs of probabilistic programs. eRHL is quantitative, i.e., its pre- and post-conditions take values in the extended non-negative reals. Thanks to its quantitative assertions, eRHL overcomes randomness alignment restrictions from prior logics, including PRHL, a popular relational program logic used to reason about security of cryptographic constructions, and apRHL, a variant of PRHL for differential privacy. As a result, eRHL is the first relational probabilistic program logic to be supported by non-trivial soundness and completeness results for all \emph{almost surely terminating} programs. We show that eRHL is sound and complete with respect to program equivalence, statistical distance, and differential privacy. We also show that every PRHL judgment is valid iff it is provable in eRHL. We showcase the practical benefits of eRHL with examples that are beyond reach of PRHL and \APRHL.

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