POPL 2025 (series) / LAFI 2025 (series) / LAFI 2025 /
Reasoning About Sampling Without Sampling: Atomic Machines for Contextual Equivalence in Probabilistic Programs
Recent approaches to probabilistic programming take a nominal approach, leveraging an analogy between probabilistic sampling and fresh name generation in the $\nu$-calculus. Proving contextual equivalences in either setting is subtle, and the semantics for the $\nu$-calculus inform the properties of a fully abstract semantics for probabilistic sampling. We present an abstract machine semantics for a probabilistic programming language based on the principles of atomic equivalence and the parametric logical relations to prove contextual equivalence in the $nu$-calculus. We explain how sampling is interpreted in this machine, and discuss how this process may be repeated for other abstract machines of the $\lambda$-calculus.