Email Gateway (Aug 19 2022 at 16:17): Email Gateway (Aug 19 2022 at 16:17):From: Lawrence Paulson <lp15@cam.ac.uk>
A Verified Compiler for Probability Density Functions
Manuel Eberl, Johannes Hölzl and Tobias Nipkow
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.
http://afp.sourceforge.net/entries/Density_Compiler.shtml
Larry Paulson
Last updated: Nov 21 2024 at 12:39 UTC