# Semantics for probabilistic programming: higher-order functions, continuous distributions, and soft constraints

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

## Key facts

- Cited by 12 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 19 Jan 2016.

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

- [Smoothness Analysis for Probabilistic Programs with Application to Optimised Variational Inference](https://mlsanity.com/paper/2208.10530/) (2022)
- [Declarative Probabilistic Logic Programming in Discrete-Continuous Domains](https://mlsanity.com/paper/2302.10674/) (2023)
- [Fast and Correct Gradient-Based Optimisation for Probabilistic Programming via Smoothing](https://mlsanity.com/paper/2301.03415/) (2023)
- [Likelihood Hacking in Probabilistic Program Synthesis](https://mlsanity.com/paper/2603.24126/) (2026)
- [Higher-Order Generalization Bounds: Learning Deep Probabilistic Programs via PAC-Bayes Objectives](https://mlsanity.com/paper/2203.15972/) (2022)
- [Nonparametric Involutive Markov Chain Monte Carlo](https://mlsanity.com/paper/2211.01100/) (2022)
- [The 4/δ Bound: Designing Predictable LLM-Verifier Systems for Formal Method Guarantee](https://mlsanity.com/paper/2512.02080/) (2025)
- [Control-Data Separation and Logical Condition Propagation for Efficient Inference on Probabilistic Programs](https://mlsanity.com/paper/2101.01502/) (2021)
- [Expectation Programming: Adapting Probabilistic Programming Systems to Estimate Expectations Efficiently](https://mlsanity.com/paper/2106.04953/) (2021)
- [Mixed Nondeterministic-Probabilistic Automata: Blending graphical probabilistic models with nondeterminism](https://mlsanity.com/paper/2201.07474/) (2022)
- [A meta-probabilistic-programming language for bisimulation of probabilistic and non-well-founded type systems](https://mlsanity.com/paper/2203.15970/) (2022)
- [Beyond Bayesian Model Averaging over Paths in Probabilistic Programs with Stochastic Support](https://mlsanity.com/paper/2310.14888/) (2023)

## Abstract (arXiv)

We study the semantic foundation of expressive probabilistic programming languages, that support higher-order functions, continuous distributions, and soft constraints (such as Anglican, Church, and Venture). We define a metalanguage (an idealised version of Anglican) for probabilistic computation with the above features, develop both operational and denotational semantics, and prove soundness, adequacy, and termination. They involve measure theory, stochastic labelled transition systems, and functor categories, but admit intuitive computational readings, one of which views sampled random variables as dynamically allocated read-only variables. We apply our semantics to validate nontrivial equations underlying the correctness of certain compiler optimisations and inference algorithms such as sequential Monte Carlo simulation. The language enables defining probability distributions on higher-order functions, and we study their properties.
