# A Domain Theory for Statistical Probabilistic Programming

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

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 10 Nov 2018.

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

- [Nonparametric Hamiltonian Monte Carlo](https://mlsanity.com/paper/2106.10238/) (2021)
- [ωPAP Spaces: Reasoning Denotationally About Higher-Order, Recursive Probabilistic and Differentiable Programs](https://mlsanity.com/paper/2302.10636/) (2023)
- [Fast and Correct Gradient-Based Optimisation for Probabilistic Programming via Smoothing](https://mlsanity.com/paper/2301.03415/) (2023)
- [Nonparametric Involutive Markov Chain Monte Carlo](https://mlsanity.com/paper/2211.01100/) (2022)
- [Lean Pool: An AI-Maintained Archive of Formalized Mathematics](https://mlsanity.com/paper/2609.25199/) (2026)
- [Sample-Smooth Spaces: A Convenient Category for Differentiable Probabilistic Programming](https://mlsanity.com/paper/2609.26270/) (2026)

## Abstract (arXiv)

We give an adequate denotational semantics for languages with recursive higher-order types, continuous probability distributions, and soft constraints. These are expressive languages for building Bayesian models of the kinds used in computational statistics and machine learning. Among them are untyped languages, similar to Church and WebPPL, because our semantics allows recursive mixed-variance datatypes. Our semantics justifies important program equivalences including commutativity. Our new semantic model is based on `quasi-Borel predomains'. These are a mixture of chain-complete partial orders (cpos) and quasi-Borel spaces. Quasi-Borel spaces are a recent model of probability theory that focuses on sets of admissible random elements. Probability is traditionally treated in cpo models using probabilistic powerdomains, but these are not known to be commutative on any class of cpos with higher order functions. By contrast, quasi-Borel predomains do support both a commutative probabilistic powerdomain and higher-order functions. As we show, quasi-Borel predomains form both a model of Fiore's axiomatic domain theory and a model of Kock's synthetic measure theory.