### 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

BSD License

### Topics

- Mathematics/Probability theory
- Computer science/Programming languages/Compiling

### 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

## Cite

×

Density_Compiler-AFP

    @article{Density_Compiler-AFP,
      author  = {Manuel Eberl and Johannes Hölzl and Tobias Nipkow},
      title   = {A Verified Compiler for Probability Density Functions},
      journal = {Archive of Formal Proofs},
      month   = {October},
      year    = {2014},
      note    = {\url{https://isa-afp.org/entries/Density_Compiler.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Dec 22, 2014 : Isabelle2014
- Oct 9, 2014 : Isabelle2014