# A Lambda-Calculus Foundation for Universal Probabilistic Programming

arXiv: https://arxiv.org/abs/1512.08990 · HTML: https://mlsanity.com/paper/1512.08990/

## Key facts

- Cited by 12 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 30 Dec 2015.

## Built on by (most cited first, 12 of 12)

- [Nonparametric Hamiltonian Monte Carlo](https://mlsanity.com/paper/2106.10238/) (2021)
- [Probabilistic Programming with Programmable Variational Inference](https://mlsanity.com/paper/2406.15742/) (2024)
- [The LLMbda Calculus: AI Agents, Conversations, and Information Flow](https://mlsanity.com/paper/2602.20064/) (2026)
- [Checking Trustworthiness of Probabilistic Computations in a Typed Natural Deduction System](https://mlsanity.com/paper/2206.12934/) (2022)
- [Fast and Correct Gradient-Based Optimisation for Probabilistic Programming via Smoothing](https://mlsanity.com/paper/2301.03415/) (2023)
- [Guaranteed Bounds for Posterior Inference in Universal Probabilistic Programming](https://mlsanity.com/paper/2204.02948/) (2022)
- [Nonparametric Involutive Markov Chain Monte Carlo](https://mlsanity.com/paper/2211.01100/) (2022)
- [Trustworthiness Preservation by Copies of Machine Learning Systems](https://mlsanity.com/paper/2506.05203/) (2025)
- [Mixed Nondeterministic-Probabilistic Automata: Blending graphical probabilistic models with nondeterminism](https://mlsanity.com/paper/2201.07474/) (2022)
- [Learning and Compositionality: a Unification Attempt via Connectionist Probabilistic Programming](https://mlsanity.com/paper/2208.12789/) (2022)
- [Worst-Case Analysis is Maximum-A-Posteriori Estimation](https://mlsanity.com/paper/2310.09774/) (2023)
- [Beyond Bayesian Model Averaging over Paths in Probabilistic Programs with Stochastic Support](https://mlsanity.com/paper/2310.14888/) (2023)

## Abstract (arXiv)

We develop the operational semantics of an untyped probabilistic lambda-calculus with continuous distributions, as a foundation for universal probabilistic programming languages such as Church, Anglican, and Venture. Our first contribution is to adapt the classic operational semantics of lambda-calculus to a continuous setting via creating a measure space on terms and defining step-indexed approximations. We prove equivalence of big-step and small-step formulations of this distribution-based semantics. To move closer to inference techniques, we also define the sampling-based semantics of a term as a function from a trace of random samples to a value. We show that the distribution induced by integrating over all traces equals the distribution-based semantics. Our second contribution is to formalize the implementation technique of trace Markov chain Monte Carlo (MCMC) for our calculus and to show its correctness. A key step is defining sufficient conditions for the distribution induced by trace MCMC to converge to the distribution-based semantics. To the best of our knowledge, this is the first rigorous correctness proof for trace MCMC for a higher-order functional language.