### 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 with the same title.

### License

### Topics

### Related publications

- Eberl, M., Hölzl, J., & Nipkow, T. (2015). A Verified Compiler for Probability Density Functions. Lecture Notes in Computer Science, 80–104. https://doi.org/10.1007/978-3-662-46669-8_4
- arxiv

### Session Density_Compiler

- Density_Predicates
- PDF_Transformations
- PDF_Values
- PDF_Semantics
- PDF_Density_Contexts
- PDF_Compiler_Pred
- PDF_Target_Semantics
- PDF_Target_Density_Contexts
- PDF_Compiler