A Verified Compiler for Probability Density Functions

Manuel Eberl, Johannes Hölzl, Tobias Nipkow

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