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

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.