A Verified Compiler for Probability Density Functions
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.
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}}
}