The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

There is Philippe Audebaud & Chrisine Paulin-Mohring Proofs of randomized algorithms in Coq. If memory serves, they formalise continuous probabilities in Coq. It's probably not directly relevant to your purpose but will probably be helpful.

On 4 July 2014 16:54, Kevin Sullivan <sullivan.kevinj AT gmail.com> wrote:

​I'm interested in representing and reasoning about stochastic/probabilistic models, such as Bayesian networks​, using Coq. I'm looking for pointers to the most relevant available on, or relating to, this area. If you have advice or pointers, I'd appreciate having your input. I've done some homework and found CPM's work on monadic interpretations of probabilistic programs and work by Bhat et al. on a type theory for continuous probability distributions. Is there anything else out there?

Background on BN's (discrete distribution case).

A Bayesian network is a pair (D, P), where D = V, E is a directed a-cyclic graph with domain nodes, V = {V1,...,Vn}, and directed edges Vi, Vj ∈ E and where P, the joint probability distribution over V is defined as the product, over the Vi, of the conditional probability of Vi given its parent nodes in the digraph.

For now, I assume that all nodes have associated discrete probability distributions. So, in principle, the conditional probabilities can be given by tables. What I need, it appears, is a library for representing and reasoning with conditional probabilities -- and products thereof (joint probability distributions).

Thanks,

Kevin