Oct 11 2010
Lundi 11/10/2010, à partir de 11h, en salle Euler Bleu.
Orateur : Guillaume Cano.
Titre : La vérification formelle du théorème de Perron-Frobenius.
Résumé :
La présentation portera sur le théorème de Perron-Frobenius, ça parle de matrices, de valeurs propres et de rayon spectrale. J’essaierai de présenter un peu la démonstration du théorème, et ce que j’ai formalisé i.e. les nombres complexes, quelques points de la démonstration et un peu de topologie.
Sep 09 2010
Jeudi 09/09/2010, à partir de 16h, en salle Galois Coriolis.
Orateur : Sylvain Heraud.
Titre : Formaliser des fonctions polynomiales en Coq.
Résumé :
Nous présenterons deux classes de complexité, Cobham [Cob64] et Bellantoni/Cook [BS92], qui permettent de décrire tout les programmes polynomiales (et uniquement les programmes polynomiales). L’article de Bellantoni et Cook [BC92] montre que ces deux classes sont équivalentes, nous vous montrerons comment on peut traduire cette preuve en un compilateur certifie en Coq. Ces résultats pourront être utiliser en Cryptographie [BGZ09, Now07], ou en Complexite [SJ03] (si vous en connaissez d’autres preuves qui on besoin de la notion « Polytime » je suis preneur). Ça peut être un premier pas vers la formalisation de classes plus complexes comme [Hof00] ou plus récemment [Zha09].[BGZ09] G. Barthe, B. Gregoire, and S. Zanella Béguelin. Formal certification of code-based cryptographic proofs. POPL.
[BC92] S. Bellantoni and S.A. Cook. A new recursion-theoretic characterization of the polytime functions. Computational Complexity.
[Cob64] A. Cobham. The intrinsic computational difficulty of functions. International Congress for Logic, Methodology, and the Philosophy of Science.
[Hof00] M. Hofmann. Safe recursion with higher types and BCK-algebra. Annals of Pure and Applied Logic.
[Now07] D. Nowak. A framework for game-based security proofs. ICICS 2007.
[SJ03] C. Schurmann and J. Shah. Representing reductions of NP-complete problems in logical frameworks: a case study. MERLIN.
[Zha09] Y. Zhang. The Computational SLR: A Logic for Reasoning about Computational Indistinguishability. TLCA.
Jun 30 2010
Mercredi 30/06/2010, à partir de 11h, en salle Byron Blanc.
Orateur : Michaël Armand.
Titre : De SAT à SMT.
Résumé :
Pour ceux qui n’y ont pas encore eu droit, je vous montrerais comment on utilise un solveur SAT pour construire un solveur SMT : Satisfiability Modulo Theories. J’illustrerais le principe avec une théorie particulière (EUF soit Equality with Uninterpreted Functions), et je montrerais comment combiner plusieurs théories pour en arriver à un solveur SMT performant. Enfin, j’expliquerais comment faire on peut faire croire ça à Coq!
Jun 25 2010
Vendredi 25/06/2010, à partir de 11h, en salle Byron Blanc.
Orateur : Érik Martin-Dorel.
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-Raphson, au sens où les fonctions considérées sont des polynômes à coefficients entiers.Outre son intérêt propre pour déterminer les racines entières de polynômes sur Z, la technique de calcul proposée par ce lemme est, dans sa version bivariée, intensivement utilisé par l’algorithme SLZ (Stehlé/Lefèvre/Zimmermann) conçu pour résoudre de manière exacte ce qu’on appelle le Dilemme du fabricant de tables.
La formalisation puis la preuve de ce lemme dans un système formel tel que Coq est donc essentielle pour le processus de validation de ce type d’algorithme, dont la complexité intrinsèquement exponentielle donne des temps de calcul considérables. Nous présenterons ainsi les diverses étapes que nous avons rencontées lors de la formalisation du lemme de Hensel univarié en SSReflect, ainsi que les pistes envisagées pour la suite de cette formalisation.
Jun 09 2010
Mercredi 09/06/2010, à partir de 11h, en salle Galois Coriolis.
Orateur : Nicolas Julien.
Titre : Effective and sequential definition by cases on the reals via infinite signed-digit numerals by M. Escardo.
Résumé :
Je vais parler d’un résultat amusant en arithmétique réelle. Il est possible de calculer certaines fonctions définies par cas même si la comparaison n’est pas décidable. Dans son article, Martin Escardo montre la calculabilité d’un opérateur général défini par cas dans un cadre où les réels sont représentés par des suites infinies de chiffres signés en base deux. Je vais présenter les étapes de sa preuve.L’article de M. Escardo peut être trouvé ici : http://www.cs.bham.ac.uk/~mhe/papers/lexnew.pdf
