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.
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}"
}