Contenu de ce dossier
---------------------

Les sources Coq de la formalisation des théories ainsi que des
démonstrations de correction des algorithmes.

proba.v : la théorie de la mesure et des probabilités, en Coq.

lo_axiom.v : la théorie des flots et le langage de formules LO (pour
les démonstrations sur les formules générées par le transformateur PI)

bernoulli.lo : le code source en Lambda-O d'un algorithme de simulation de
la distribution de Bernoulli. Celui-là même que l'on passe au
transformateur PI.

bernoulli.v : la <<fiche de preuve>>, à partir de la formule générée par
PI, de la terminaison et de la correction de l'algorithme de simulation de
la distribution de Bernoulli contenu dans le fichier bernoulli.lo.

expo.* : pareil, pour la distribution exponentielle.

binomial.* : distribution binomiale.

geometric.* : distribution géométrique.


Dépendances :
- lo_axiom.v dépend de proba.v
- bernoulli.v, expo.v, binomial.v, geometric.v dépendent de lo_axiom.v et
donc aussi de proba.v

ATTENTION : Les fichiers *.v sont en Coq V8.0.