A verified compiler for probability density functions

DOI10.1007/978-3-662-46669-8_4MaRDI QIDQ2802431zbMATH OpenOpenAlexFDO

Authors Manuel Eberl, Johannes Hölzl, Tobias Nipkow

Publication date 26 April 2016

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1707.06901

Mathematics Subject Classification ID

Theory of compilers and interpreters (68N20)

Abstract: Bhat et al. developed an inductive compiler that computes density functions for probability spaces described by programs in a simple 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, using a standard refinement approach: first, an abstract compiler working with abstract functions modelled directly in the theorem prover's logic is defined and proven sound. Then, this compiler is refined to a concrete version that returns a target-language expression.

Recommendations

• Deriving probability density functions from probabilistic functional programs
• Deriving probability density functions from probabilistic functional programs
• Deriving a probability density calculator (functional pearl)
• A verified compiler from Isabelle/HOL to CakeML
• A formally verified compiler back-end

Cited in

(13)

• Deriving probability density functions from probabilistic functional programs
• Deriving probability density functions from probabilistic functional programs
• Density Compiler
• Program logic for higher-order probabilistic programs in Isabelle/HOL
• Verified analysis of random binary tree structures
• Equational Reasoning with Applicative Functors
• A formalization of the Lévy-Prokhorov metric in Isabelle/HOL
• Derandomization with pseudorandomness
• Effect polymorphism in higher-order logic (proof pearl)
• Effect polymorphism in higher-order logic (proof pearl)
• Markov chains and Markov decision processes in Isabelle/HOL
• A software tool for automatically verified operations on intervals and probability distributions
• A formalized hierarchy of probabilistic system types. Proof pearl

Describes a project that uses

Uses Software

• pGCL
• Isabelle/HOL
• Isabelle
• Coq

This page was built for publication: A verified compiler for probability density functions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2802431)