POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France
Sun 11 Jan 2026 14:12 - 14:22 at Salle 13 - Third Session Chair(s): Cameron Freer

The notion of contextual equivalence in higher-order probabilistic programming languages captures the idea that two programs are indistinguishable when placed in any context — where contexts themselves are programs written in the same language. In a probabilistic setting, this idea can be naturally quantified, leading to the concept of contextual distance: the distance between two programs M and N is defined as the supremum of the difference that any context can observe in the behavior of M and N.

However, when copying of arguments by contexts is allowed and all programs terminate, this distance becomes trivial: any two non-equivalent programs are then always at maximal distance. In this work, we present a new proof of this trivialization phenomenon based on the weak law of large numbers, replacing purely analytic reasoning with probabilistic arguments. We then apply this approach to study amortized and graded variants of contextual distance, deriving explicit lower bounds using affine contexts and classical probabilistic tools such as the Central Limit Theorem, the Berry–Esseen theorem, and the Chernoff–Hoelding inequalities.

Sun 11 Jan

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

14:00 - 15:30
Third SessionLAFI at Salle 13
Chair(s): Cameron Freer Massachusetts Institute of Technology
14:00
10m
Talk
Towards Compiling Higher-Order Programs to Bayesian Networks
LAFI
Claudia Faggian CNRS, Université Paris Cité, Gabriele Vanoni IRIF, Université Paris Cité
14:12
10m
Talk
On Contextual Distances in Randomized Programming: Amplification and Lower Bounds
LAFI
14:24
10m
Talk
Nominal Semantics for First-class Automatic Differentiation
LAFI
Jack Czenszak Yale University, Alexander K. Lew Yale University
14:36
10m
Talk
Semantic Foundations for Laziness in Discrete Probabilistic Programming
LAFI
Simon Castellan University of Rennes; Inria; CNRS; IRISA, Tom Hirschowitz Univ. Grenoble Alpes, Univ. Savoie Mont Blanc, CNRS, LAMA, 73000 Chambéry, Hugo Paquet Inria, École Normale Supérieure
14:48
10m
Talk
Incremental Density Computation for Efficient Programmable Inference
LAFI
Fabian Zaiser MIT, Vikash Mansinghka Massachusetts Institute of Technology, Alexander K. Lew Yale University
15:00
10m
Talk
Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops
LAFI
Kevin Batz , Adrian Gallus RWTH Aachen University, Darion Haase RWTH Aachen University, Benjamin Lucien Kaminski Saarland University; University College London, Joost-Pieter Katoen RWTH Aachen University, Lutz Klinkenberg RWTH Aachen University, Tobias Winkler RWTH Aachen University
15:12
10m
Talk
Probabilistic Programming Meets Automata Theory: Exact Inference using Weighted Automata
LAFI
Dominik Geißler Technische Universität Berlin, Tobias Winkler RWTH Aachen University
File Attached