# A Verified Compiler for Probability Density Functions

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 21 Jul 2017.

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

- [Formally Certified Approximate Model Counting](https://mlsanity.com/paper/2406.11414/) (2024)
- [Formally Verified Solution Methods for Infinite-Horizon Markov Decision Processes](https://mlsanity.com/paper/2206.02169/) (2022)

## Abstract (arXiv)

Bhat et al. developed an inductive compiler that computes density functions for probability spaces described by programs in a simple probabilistic functional language. In this work, we implement such a compiler for a modified version of this language within the theorem prover Isabelle and give a formal proof of its soundness w.r.t. the semantics of the source and target language. Together with Isabelle's code generation for inductive predicates, this yields a fully verified, executable density compiler. The proof is done in two steps, using a standard refinement approach: first, an abstract compiler working with abstract functions modelled directly in the theorem prover's logic is defined and proven sound. Then, this compiler is refined to a concrete version that returns a target-language expression.