TY - GEN
T1 - A verified compiler for probability density functions
AU - Eberl, Manuel
AU - Hölzl, Johannes
AU - Nipkow, Tobias
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2015.
PY - 2015
Y1 - 2015
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84926613795&partnerID=8YFLogxK
U2 - 10.1007/978-3-662-46669-8_4
DO - 10.1007/978-3-662-46669-8_4
M3 - Conference contribution
AN - SCOPUS:84926613795
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 80
EP - 104
BT - Programming Languages and Systems - 24th European Symposiumon Programming, ESOP 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, Proceedings
A2 - Vitek, Jan
PB - Springer Verlag
T2 - 24th European Symposium on Programming, ESOP 2015 held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015
Y2 - 11 April 2015 through 18 April 2015
ER -