Density Compiler

MaRDI QIDQ40373swMATHFDO

Authors Manuel Eberl, Johannes Hölzl, Tobias Nipkow

Publication date 9 October 2014

Official website https://www.isa-afp.org/entries/Density_Compiler.html

Cites work

• Deriving probability density functions from probabilistic functional programs

Described by source

• A verified compiler for probability density functions

Cited in

(30)

• Markov chains and Markov decision processes in Isabelle/HOL
• HOL-Omega
• Program logic for higher-order probabilistic programs in Isabelle/HOL
• pGCL
• Equational Reasoning with Applicative Functors
• Tycon
• Ergodic theory
• Zoo Probabilistic Systems
• Jordan Normal Forms
• Markov Models
• CryptHOL
• Monomorphic Monad
• Applicative Lifting
• Meta Model Isabelle
• Perron Frobenius
• Amortized Complexity
• Social Choice Theory
• QuickSort Cost
• Treaps
• Stable Matching
• Arrow Gibbard Satterthwaite
• Root Balanced Tree
• Random BSTs
• Probabilistic_While
• Monad normalisation
• Probabilistic_Prime_Tests
• Verified analysis of random binary tree structures
• Verified analysis of random binary tree structures
• Effect polymorphism in higher-order logic (proof pearl)
• Quasi-Borel Spaces

This page was built for software: Density Compiler