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.
