Résumé de séminaire

Projet ProVal
Pôle Commun de Recherche en Informatique du plateau de Saclay
CNRS, Ecole Polytechnique, INRIA, Université Paris-Sud.

Résumé :

Les programmes aléatoires jouent un rôle important que ce soit pour trouver des solutions approchées efficaces à des problèmes complexes, ou pour construire des algorithmes distribués équitables ou encore pour modéliser des environnements incertains. Dans cet exposé, nous présentons un environnement de modélisation et de raisonnement sur des programmes séquentiels probabilistes réalisé dans le système Coq. Cet environnement repose sur une transformation monadique d'un mini-langage fonctionnel avec primitives aléatoires. Chaque programme est interpréte comme une mesure, ce qui permet d'analyser directement la probabilité que le résultat de l'évaluation de ce programme satisfasse une propriété donnée. Nous proposons également des règles dérivées en particulier pour analyser un programme construit par point fixe. La méthode est illustrée sur des exemples élémentaires de simulation de différentes distribution.

Références :

Home-page : http://www.lri.fr/~paulin/
Article soumis: http://www.lri.fr/~paulin/ALEA/article.pdf
Contrat decrivant la bibliotheque: http://www.lri.fr/~paulin/ALEA/library.pdf