Category: Séminaires

(English) Talk by Claudio Sacerdoti Coen

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

(English) Talk by Tsvetan Chavdarov Dunchev

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

Exposé par Isabella Dramnesc (en anglais)

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

Séminaire Marelle: Proofs as documents: asynchronous interaction for Coq

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

Séminaire Marelle : A Coq formalization of finitely presented modules.

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

Séminaire Marelle : Types and Data types in Continuation Calculus and lambda calculus

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

Séminaire Marelle : Certified, Efficient and Sharp Univariate Taylor Models in COQ.

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

Séminaire Marelle : Sur la théorie des types homotopiques

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.

Séminaire Marelle : Automatisation de preuves en Coq par traduction en logique du premier ordre

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.

Séminaire Marelle : Le théorème des trois cercles

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.