Abstract: 
Bhat et al. [TACAS 2013] developed an inductive compiler that computes
density functions for probability spaces described by programs in a
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: First, an abstract compiler
working with abstract functions modelled directly in the theorem prover's
logic is defined and proved sound. Then, this compiler is refined to a
concrete version that returns a targetlanguage expression.
An article with the same title and authors is published in the proceedings
of ESOP 2015.
A detailed presentation of this work can be found in the first author's
master's thesis. 
BibTeX: 
@article{Density_CompilerAFP,
author = {Manuel Eberl and Johannes Hölzl and Tobias Nipkow},
title = {A Verified Compiler for Probability Density Functions},
journal = {Archive of Formal Proofs},
month = oct,
year = 2014,
note = {\url{http://isaafp.org/entries/Density_Compiler.html},
Formal proof development},
ISSN = {2150914x},
}
