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)


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)


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

Download BibTeX (297 Bytes)