Isabelle logo

Manuel Eberl

Chair for Logic and Verification

A Verified Compiler for Probability Density Functions

by Manuel Eberl

Master's thesis at the Technical University of Munich (2014)

Abstract:

Bhat et al. developed an inductive compiler that computes density functions for probability spaces described by programs in a probabilistic functional language. In this thesis, we implemented 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.

Download PDF (302 KiB)

BibTeX:

@mastersthesis{eberl14,
 author = {Eberl, Manuel},
 title = {A Verified Compiler for Probability Density Functions},
 year = {2014},
 month = {10},
 school = {Technical University of Munich},
 type = {Master's thesis},
 note = {\url{https://www21.in.tum.de/~eberlm/pdfs/pdfcompiler.pdf}}
}

Download BibTeX (290 Bytes)