Tag: assistant de preuve

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

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

Soutenance de Thèse : Étude formelle d’algorithmes efficaces en algèbre linéaire

Le mercredi 20/11/2013, à partir de 13h30 à la salle de conférence I3S.

Orateur : Maxime Denès.
Titre : Étude formelle d’algorithmes efficaces en algèbre linéaire.

Résumé : Les méthodes formelles ont atteint un degré de maturité conduisant à la
conception de systèmes de preuves généralistes, permettant à la fois de
vérifier la correction de systèmes logiciels complexes ou de formaliser des
mathématiques avancées. Mais souvent, l’accent est mis davantage sur la
facilité du raisonnement sur les programmes plutôt que sur leur exécution
efficace. L’antagonisme entre ces deux aspects est particulièrement sensible
pour les algorithmes de calcul formel, dont la correction repose habituellement
sur des concepts mathématiques élaborés, mais dont l’efficacité pratique
est une préoccupation importante.
Cette thèse développe des approches à l’étude formelle et l’exécution efficace
de programmes en théorie des types, et plus précisément dans l’assistant à la
preuve Coq. Dans un premier temps, nous présentons un environnement
d’exécution permettant de compiler en code natif de tels programmes tout
en conservant la généralité et l’expressivité du formalisme.
Puis, nous nous intéressons aux représentations de données et plus
particulièrement au lien formellement vérifié et automatisé entre représentations
adaptées aux preuves ou au calcul.
Ensuite, nous mettons à profit ces techniques pour l’étude d’algorithmes
en algèbre linéaire, comme le produit matriciel de Strassen, le procédé
d’élimination de Gauss ou la mise en forme canonique de matrices, dont
notamment la forme de Smith pour les matrices sur un anneau euclidien.
Enfin, nous ouvrons le champ des applications à la formalisation et au calcul
certifié des groupes d’homologie de complexes simpliciaux issus d’images
numériques.

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

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

Démonstration du théorème Feit-Thompson : La précision des ordinateurs au service des mathématiques

http://www.inria.fr/centre/sophia/actualites/la-precision-des-ordinateurs-au-service-des-mathematiques

Démonstration du théorème Feit-Thompson : Un grand succès pour la preuve informatique

http://www.inria.fr/centre/saclay/actualites/un-grand-succes-pour-la-preuve-informatique

The Coq proof assistant is the recipient of the 2013 software award

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

Coq, les maths ont trouvé leur maître (Article de Science et Vie magazine)

Article de Science et Vie (PDF)

A Machine-Checked Proof of the Odd Order Theorem

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