Density Compiler
| swMATH ID: | 28659 |
| Software Authors: | Eberl, Manuel; Hölzl, Johannes; Nipkow, Tobias |
| Description: | A Verified Compiler for Probability Density Functions. 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. |
| Homepage: | https://www.isa-afp.org/entries/Density_Compiler.html |
| Dependencies: | Isabelle |
| Related Software: | Isabelle/HOL; HOL; Archive Formal Proofs; Isabelle; Coq; Lifting; Transfer; pGCL; Ergodic theory; Random BSTs; Root Balanced Tree; Treaps; QuickSort Cost; Amortized Complexity; CryptHOL; Zoo Probabilistic Systems; HOL-Omega; PRISM; ML; Lean |
| Cited in: | 7 Documents |
Standard Articles
| 1 Publication describing the Software, including 1 Publication in zbMATH | Year |
|---|---|
|
A verified compiler for probability density functions. Zbl 1335.68037 Eberl, Manuel; Hölzl, Johannes; Nipkow, Tobias |
2015
|
all
top 5
Cited by 9 Authors
| 3 | Eberl, Manuel |
| 3 | Nipkow, Tobias |
| 2 | Haslbeck, Max W. |
| 2 | Hölzl, Johannes |
| 2 | Lochbihler, Andreas |
| 1 | Hirata, Michikazu |
| 1 | Minamide, Yasuhiko |
| 1 | Sato, Tetsuya |
| 1 | Schneider, Joshua P. |
Cited in 1 Serial
| 3 | Journal of Automated Reasoning |
Cited in 4 Fields
| 7 | Computer science (68-XX) |
| 1 | Category theory; homological algebra (18-XX) |
| 1 | Probability theory and stochastic processes (60-XX) |
| 1 | Operations research, mathematical programming (90-XX) |
