Category: Séminaires

Sep 08 2015

(English) Talk by Claudio Sacerdoti Coen

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

Jul 09 2015

(English) Talk by Tsvetan Chavdarov Dunchev

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

Jun 11 2015

Exposé par Isabella Dramnesc (en anglais)

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

Jan 29 2015

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

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

Nov 22 2013

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

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

Nov 20 2013

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

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

Aug 26 2013

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

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

Aug 06 2013

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.

Jul 17 2013

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.

Jul 08 2013

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.