Mercredi 17/07/2013, à partir de 10h30, en salle Byron Blanc.

Orateur : Antoine Grospellier.

Titre : Automatisation de preuves en coq par traduction en logique du premier ordre.

Résumé :
J’ai essayé de comprendre le fonctionnement des logiciels why (et sa tactique coq) et isabelle (principalement sa fonction sledgehammer). Maintenant je tente de modifier why pour prouver un maximum de lemmes de la bibliothèque de ssreflect automatiquement.

Lundi 08/07/2013, à partir de 14h30, en salle Byron Blanc.

Oratrice : Julianna Zsido.

Titre : Le théorème des trois cercles.

Abstract:
The theorem of three circles in real algebraic geometry guarantees the termination and correctness of an algorithm of isolating real roots of a univariate polynomial. The main idea of its proof is to consider polynomials whose roots belong to a certain area of the complex plane delimited by straight lines. After applying a transformation involving inversion this area is mapped to an area delimited by circles. We provide a formalisation of this rather geometric proof in Ssreflect, allowing us to formalise the proof from an algebraic point of view.

Mardi 11/06/2013, à partir de 10h15, en salle Byron Blanc.

Orateur : Érik Martin-Dorel.

Titre : Vérification formelle de certificats fondés sur le lemme de Hensel.

Résumé :
Dans cet exposé, je présenterai les travaux effectués dans le cadre du projet TaMaDi visant à certifier formellement les résultats des algorithmes conçus pour trouver les pires cas pour l’arrondi correct des fonctions mathématiques. Les calculs menant à ces pires cas sont très longs (plusieurs années⋅CPU) et sont effectués en utilisant des programmes largement optimisés qui implantent des algorithmes très complexes. D’où l’intérêt d’utiliser un outil formel d’aide à la preuve tel que le logiciel COQ, afin de garantir formellement la correction de ces données numériques.

Dans ce travail, nous nous intéressons en particulier à l’algorithme Stehlé-Lefèvre-Zimmermann, qui consiste en une phase de découpage du domaine et d’approximation polynomiale, suivie de la résolution de myriades d’instances du problème ISValP (Integer Small Value Problem), qui revient grosso modo à trouver toutes les petites valeurs d’un polynôme à coefficients entiers, modulo un grand entier. La dernière étape de ces calculs s’appuie notamment sur la version bivariée du lemme de Hensel.

Le lemme de Hensel est un outil clé en calcul formel qui, étant donné un polynôme sur les entiers et une racine modulo un nombre premier p, construit itérativement des racines modulo p^2k, sous des hypothèses faciles à vérifier. La force du lemme de Hensel réside notamment en la présence d’une assertion d’existence (il existe un relèvement) et d’unicité (ce relèvement est unique). Nous avons formalisé ce dernier résultat (dans les cas univarié ainsi que bivarié) au sein d’une bibliothèque pour l’assistant de preuves COQ.

En s’appuyant sur ces preuves formelles, nous avons conçu puis formellement prouvé un vérificateur de certificats pour le problème ISValP. Nous avons également rendu effectif ce vérificateur de certificats, dont je présenterai plusieurs benchmarks.

Désolé, cet article est seulement disponible en Anglais Américain.

Mardi 19/03/2013, à partir de 14h, en salle Byron Blanc.

Orateur : José Grimm.

Titre : Ordinaux et récursivité.

Résumé :
Dans la théorie des ensembles de Zermelo Fraenkel on peut définir un type particulier d’ensembles, les ordinaux, avec des opérations (somme, produit, puissance), et une relation d’ordre compatible avec les opérations. Les ordinaux généralisent les entiers naturels. Beaucoup de preuves se font par induction transfinie (une variante de l’induction sur les entiers). Il y a beaucoup trop d’ordinaux pour en faire un ensemble (ou un type Coq). On peut définir (par induction transfinie) des suites d’ordinaux epsilon(x), Gamma(x), etc. Si E est l’ensemble des ordinaux plus petits que epsilon(0) ou Gamma(0), E est stable par addition, multiplication, exponentiation, et est dénombrable. On peut le définir dans Coq comme un sous-type inductif via un constructeur constant zero, et un autre de type E→nat→E→E ou E→E→nat→E→E. Je montrerai le lien entre mon implémentation des ordinaux de Bourbaki, et les travaux de Pierre Castéran.

Lundi 18/02/2013, à partir de 15h30, en salle Byron Blanc.

Orateur : Érik Martin-Dorel.

Titre : Du lemme de Hensel aux certificats ISValP.

Résumé :
Le lemme de Hensel est un outil clé en calcul formel qui, étant donné un polynôme sur les entiers et une racine modulo p, construit itérativement des racines modulo p^2k, sous des hypothèses faciles à vérifier. La force du lemme de Hensel réside notamment en la présence d’une assertion d’existence et d’unicité. Nous avons formalisé ce dernier résultat dans les cas univarié ainsi que bivarié au sein de la bibliothèque CoqHensel (en utilisant Ssreflect). Puis nous avons déduit de ce résultat la correction d’un vérificateur de certificats pour le problème des petites racines entières d’un polynôme (ou de deux polynômes bivariés). En s’appuyant sur ce vérificateur bivarié, nous avons alors formalisé un vérificateur pour le problème ISValP (Integer Small Value Problem), dont le but ultime est de certifier formellement les pires cas pour l’arrondi correct des fonctions élémentaires. Enfin, à l’aide du système de modules de Coq et des bibliothèques BigZ, Flocq et Coq.Interval, nous avons rendu effectifs ces vérificateurs de certificats, dont je présenterai quelques benchmarks.

Mardi 29/01/2013, à partir de 10h30, en salle Byron Blanc.

Orateur : Guillaume Cano.

Titre : Forme normale de Frobenius et de Jordan d’une matrice.

Résumé :
Nous verrons comment a été formalisé la notion de matrice diagonale par blocs. Nous verrons ensuite comment à partir de cette notion et de la forme normale de Smith nous obtenons les forme normales de Frobenius et de Jordan d’une matrice.

Jeudi 09/08/2012, à partir de 14h, en salle Byron Blanc.

Orateur : Thomas Williams.

Titre : Vérification automatique de propriétés de « differential privacy ».

Résumé :
On cherche à montrer que des programmes faisant intervenir des tirages aléatoires ne révèlent pas trop d’informations sur leur entrée : la distribution des valeurs de sortie varie peu quand l’entrée varie peu.