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

This program is tentative and subject to change.

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

Deciding termination is a fundamental problem in the analysis of probabilistic imperative programs. We consider the qualitative and quantitative probabilistic termination problems for an imperative programming model with discrete probabilistic choice and demonic bounded nondeterminism. The qualitative question asks if the program terminates almost-surely, no matter how nondeterminism is resolved. The quantitative question asks for a bound on the probability of termination. Despite a long and rich literature on the topic, no sound and relatively complete proof systems were known for these problems. In this paper, we provide sound and relatively complete proof rules for proving qualitative and quantitative termination in the assertion language of arithmetic. Our rules use variant functions as measures of distances to termination as well as supermartingales that restrain the growth of these variants almost surely. Our completeness result shows how to construct suitable supermartingale and variant functions from an almost-surely terminating program. We also show that proofs of termination in many existing proof systems can be transformed to proofs in our system, pointing to its applicability in practice. As an application of our proof rule, we show an explicit proof of almost-sure termination for the two-dimensional random walker.

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