A Verified Compiler for Probability Density Functions
Bhat et al. [TACAS 2013] developed an inductive compiler that computes density functions for probability spaces
described by programs in a probabilistic functional language. 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 target-language expression.
pdf
BibTeX:
@inproceedings{EberlHN-ESOP05,
author = {Manuel Eberl and Johannes H\"olzl and Tobias Nipkow},
title = {A Verified Compiler for Probability Density Functions},
booktitle = {European Symposium on Programming (ESOP 2015)},
editor = {J. Vitek},
series = LNCS,
publisher = Springer,
volume = "9032",
pages = "80-104",
year = 2015
}
Isabelle theories in the
Archive of Formal Proofs