Mercredi 7 Avril, à 10h30 salle 117:
Franck
Butelle (LIPN, Université Paris 13)
Titre: Preuve formelle de la fonction conjuguée du logiciel SCHUR
Résumé:
(Travail en commun avec Florent Hivert, Micaela Mayero et Frédéric Toumazet)
Nous présenterons une preuve formelle de correction d'une fonction clé
du logiciel SCHUR, programme C interactif de calcul des
caractères des groupes de Lie et des fonctions symétriques.
Ces calculs reposent sur l'énumération et la manipulation de
structures combinatoires. La preuve de la fonction conjuguée
doit être vue comme une démonstration de faisabilité.
Pour prouver formellement cette fonction, nous avons utilisé Frama-C. A
partir d'annotations des programmes C, il génère les obligations de preuves qui
seront prouvées par des prouveurs automatiques. Nous
présentons également une esquisse de méthodologie pour prouver ce
type de programmes.
Jeudi 18 Mars, à 10h30 salle 117:
Milad Niqui (Centrum Wiskunde & Informatica, Amsterdam)
Titre: CoRN and Reals: merging two Coq libraries of real numbers?
Résumé:
(joint work with Micaela Mayero)
There exist some Coq libraries of real numbers. Two of them, CoRN and
Reals, are intensively used by users. These libraries are different
in several aspects we will expose. In our work, we make some
reflexions with the goal to merge a part of these libraries. We
discuss on theoretical problems and try to give some solutions.
Mercredi 10 Mars 2010, à 10h30 salle 117 :
Erik Martin-Dorel (LIP / Arénaire)
Titre: Formalisation du lemme de Hensel en Coq
Résumé:
Le lemme de Hensel est un résultat d'arithmétique qui peut être vu
comme l'analogue discret de la méthode de Newton, permettant de donner
des approximations de racines des polynômes.
La technique de calcul proposée par ce lemme étant très efficace en
pratique, elle est intensivement utilisée par l'un des principaux
algorithmes conçus pour résoudre le dilemme du fabricant de tables de
manière exacte.
La formalisation puis la preuve du lemme de Hensel dans un système
formel tel que Coq est donc une étape essentielle pour le processus de
validation de ce type d'algorithme. Nous présenterons ainsi nos
premiers développements réalisés en Coq et avec l'extension SSReflect
pour formaliser le lemme de Hensel univarié.
Mercredi 20 janvier 2010, à 10h30 salle 116:
Valentin Blot (ENS Lyon),
Titre: Nombres algébriques en Coq
Résumé:
On présentera une étude sur la formalisation des nombres algébriques en coq.
Cet exposé pourra prendre deux directions différentes, suivant l'intérêt du
public. Une première possibilité serait de montrer en quoi la formalisation de
la division euclidienne de polynômes et du théorème de Cayley-Hamilton
constituent une première étape dans cette formalisation, puis de donner
quelques idées de la "bonne" manière de voir les extensions algébriques.
L'autre possibilité serait de présenter la formalisation du théorème de
Liouville qui dit que tout nombre irrationnel algébrique est en un certain
sens "distant" de tout nombre rationnel, résultat qui repose sur le théorème
de Rolle (déjà formalisé dans C-CoRN) et sur un algorithme certifié
d'extraction des racines rationnelles d'un polynôme à coefficients rationnels
qui sera donc présenté.
Mercredi 6 janvier 2010, à 10h30 salle 117:
Philippe Audebaud (LIP / Plume),
Titre: Hasard et Nécessité
Résumé:
Les algos probabilistes sont très utiles et souvent indispensables.
Ils ont la réputation de fournir souvent des implantations simples,
laissant la part la plus pénible à la preuve de leur correction.
Dans ce contexte, l'assistant de preuve Coq, malgré sa puissance, se
trouve confronté à des problèmes qui ne rentrent pas dans son cadre :
non déterminisme, non terminaison, etc.
A l'aide de quelques petits exemples, je montrerai comment un peu de
pragmatisme permet de trouver des solutions utiles malgré tout, ainsi
que les défis encore posés aux mathématiques en présence de programmes
aléatoires fonctionnels.
Mercredi 2 décembre 2009, à 10h30 salle 117:
Christophe Mouilleron (LIP / Arénaire),
Titre: L'arithmétique virgule flottante en Coq
Résumé:
Gappa est un outil permettant de vérifier des propriétés numériques
sur des programmes utilisant des nombres flottants. On peut demander
à l'outil de générer les preuves Coq des résultats annoncés. Ces preuves
s'appuient sur des théorèmes prouvés dans la librairie gappalib-coq.
La librairie Float fournit elle aussi un ensemble de définitions et
de théorèmes sur les nombres flottants. L'approche est assez différente
de celle de la libraire gappalib-coq, et apporte un cadre plus pratique
et plus riche pour faire des preuves.
Après une présentation de ces deux librairies, nous verrons comment
prouver certains résultats utilisés dans la librairie d'arithmétique
virgule flottante multi-précision MPFR.
Mercredi 18 novembre 2009, à 10h30 salle 117:
Jean Duprat (LIP / Plume),
Titre: La géométrie d'Euclide à la règle et au compas
Résumé:
On se propose de définir la géométrie d'Euclide à partir des
primitives de construction à la règle et au compas. Nous verrons
que cette façon de formaliser la géométrie plane conduit à devoir
préciser les notions liées à l'orientation et à la métrique. On
terminera par l'implantation des axiomes correspondants en Coq.
Mercredi 4 novembre 2009, à 10h30 salle 116:
Guillaume Hanrot (LIP / Arénaire),
Titre: Le dilemme du fabriquant de tables : validation, preuve ?
Résumé:
Le dilemme du fabriquant de tables est un problème d'arithmétique
flottante qui, grosso modo, demande étant donné une fonction f à
évaluer quelle est la précision des calculs intermédiaires à effectuer
pour pouvoir décider de l'arrondi correct du résultat.
Les meilleurs algorithmes connus pour résoudre exactement ce problème sont
de type semi-exhaustifs, donc intrinsèquement exponentiels en la précision
d'entrée ; cela signifie qu'on est souvent face à un long calcul produisant
une réponse oui ou non, sans garantie particulière.
Dans cet exposé, nous exposerons au public quelques pistes de validation
possibles pour ces longs calculs, avec l'espoir de déboucher sur une
discussion permettant d'éclairer quel niveau de validation est possible
et avec quelle quantité de moyens (principalement humains).
Aucune connaissance préalable en arithmétique flottante n'est requise.
Mercredi 21 octobre 2009, à 10h30 salle 116:
Thomas Braibant et
Damien Pous
(LIG / projet Sardes),
Titre: Kleene et Kozen en Coq : formalisation d'un algorithme de décision
Résumé:
Formaliser des choses dans un assistant de preuve s'avère souvent
pénible, de nombreuses étapes de raisonnement devant être explicitées
alors qu'elles sont d'habitude laissées au relecteur scrupuleux. Ceci
est en particulier vrai lorsque l'on doit travailler sur des relations
binaires (réécriture, réductions, équivalences, etc...), très
intuitives, mais pas complètement triviales.
Lorsque c'est possible, une première astuce consiste à considérer les
relations de façon algébrique : en montant le niveau d'abstraction, on
facilite la formalisation de certaines preuves. Une fois ce pas
franchi, on réalise que les relations binaires sont un modèle des
algèbres de Kleene, décidables par la théorie des automates finis.
Nous exposerons un travail récent portant sur la formalisation en Coq
d'algorithmes d'automates, afin d'obtenir une tactique de décision des
algèbres de Kleene, par réflection. Nous détaillerons également les
outils que nous avons du développer pour travailler efficacement avec
des matrices.