  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.
