A library for reasoning on randomized algorithms in Coq
Christine Paulin
This library forms a basis for reasoning on randomised algorithms in
the proof assistant Coq [3].
As proposed by Kozen [1, 2], we interpret
probabilistic programs as measure transformers; the originality of our
approach is to view this interpretation as a monadic transformation on
functional programs. Using this semantics, we derive general rules
for estimating the probability for a randomised algorithm to satisfy
certain properties. We apply this for formally proving in the proof
assistant Coq randomised algorithms such as the Bernoulli
distribution from a coin flip or the termination of a random walk.
The library is composed of the following files :

U_base
 An axiomatisation of the interval [0.1]
 U_prop
 Derived operations and properties of
operators on [0,1]
 Monads
 Definition of the basic monad for randomized constructions,
the type a is mapped to the type (a ®
[0,1])® [0,1] of measure functions.
 Probas
 Definition of a dependent type for
distributions on a type a, which is a record containing a
measure function of type (a ® [0,1])® [0,1] and proofs
that this function enjoys the measure properties of stability. We
define the interpretation of specific
random primitives.
 Prog
 Definition of randomized programs
constructions and rules for axiomatic semantics on these randomized
programs.
 IterFlip

A proof of probabilistic termination for a random walk.
 Choice
 A proof of composition of two runs of a probabilistic
program, when a choice can improve the quality of the result.
 Bernouilli
 Construction of a bernouilli distribution from
the flip distribution.
 Transitions
 A probabilistic transition
system is defined by a set of states and a probabilistic transition
function which associates to a state a the probability to go to
a state b. In our system it corresponds to a function from states to
distribution on states. We use this function in order to define
the corresponding distribution on
paths of length k for a given integer k.
References
 [1]

Dexter Kozen.
Semantics of probabilistic programs.
Journal of Computer and System Sciences, 1981.
 [2]

Dexter Kozen.
A probabilistic PDL.
In 15th ACM Symposium on Theory of Computing, 1983.
 [3]

The Coq Development Team.
The Coq Proof Assistant Reference Manual  Version V8.0,
April 2004.
.
This document was translated from L^{A}T_{E}X by
H^{E}V^{E}A.