A Verified Compiler for Probability Density Functions

Title:	A Verified Compiler for Probability Density Functions
Authors:	Manuel Eberl, Johannes Hölzl and Tobias Nipkow
Submission date:	2014-10-09
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 target-language 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_Compiler-AFP, 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://isa-afp.org/entries/Density_Compiler.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Proof outline
Proof document

Browse theories

Download this entry