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