Paper Info
Title
A Verified Compiler for Probability Density Functions.
Abstract
Bhat et al. developed an inductive compiler that computes density functions for probability spaces described by programs in a probabilistic functional language. 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.
Year
DOI
Venue
2014
10.1007/978-3-662-46669-8_4
Lecture Notes in Computer Science
DocType
Volume
ISSN
Journal
9032
0302-9743
Citations 
PageRank 
References 
4
0.51
9
Authors
3
Name
Order
Citations
PageRank
Manuel Eberl11113.27
Johannes Hölzl211613.23
Tobias Nipkow33056232.28