Isabelle logo

Manuel Eberl

Chair for Logic and Verification

A Ver­i­fied Com­piler for Prob­a­bil­ity Den­sity Func­tions

by Manuel Eberl, Johannes Hölzl, and Tobias Nipkow

In: Proceedings of ESOP 2015

DOI:

10.1007/978-3-662-46669-8_4

Abstract:

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.

Download preprint PDF (390 KiB)

BibTeX:

@inproceedings{eberl15esop,
  author = "Eberl, Manuel and H{\"o}lzl, Johannes and Nipkow, Tobias",
  editor = "Vitek, Jan",
  title = "A Verified Compiler for Probability Density Functions",
  booktitle = "Programming Languages and Systems (ESOP 2015)",
  series = "Lecture Notes in Computer Science",
  volume = "9032",
  year = "2015",
  publisher = "Springer",
  address = "Berlin, Heidelberg",
  pages = "80--104",
  doi = "10.1007/978-3-662-46669-8_4",
  isbn = "978-3-662-46669-8"
}

Download BibTeX (490 Bytes)

(The final publication is available at link.springer.com)