Reasoning About Sampling Without Sampling: Atomic Machines for Contextual Equivalence in Probabilistic Programs

Explore a 13-minute conference talk from the LAFI 2025 workshop where researchers Anthony D'Arienzo and Jon Aytac from the University of Illinois and Sandia National Laboratories present their work on probabilistic programming semantics. Learn about their novel approach that draws parallels between probabilistic sampling and fresh name generation in the ν-calculus. Discover how they developed an abstract machine semantics based on atomic equivalence and parametric logical relations to prove contextual equivalence without direct sampling. The presentation explains their interpretation of sampling within this machine framework and discusses how their methodology could extend to other abstract machines of the λ-calculus. This technical talk was presented at the LAFI workshop on January 19, 2025, as part of the POPL25 conference sponsored by ACM SIGPLAN.