Catégorie : Séminaires

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

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

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

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

Mardi 06/08/2013, à partir de 14h30, en salle Byron Blanc.

Orateur : Florent Brehard.

Titre : Sur la théorie des types homotopiques.

Résumé :
L’exposé aura une première partie sur les principes de bases des types d’homotopie.
La deuxième partie parlera plus précisément des sphères en dimension n.

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.