Formalization of efficient polyhedral computations

Formalisation de calculs polyédraux efficaces L'étude de la complexité de l'algorithme du simplexe est un problème ouvert jalonné de plusieurs événements clés. La réfutation de la conjecture de Hirsch, qui cherchaità déterminer une borne supérieure au nombre de pivots nécessaires à l'exécution de son algo-rithme, est l'une d'entre elles. Mais cette preuve a nécessité une étape de calculs numériques qui, bien que faisable à la main, montre que la nécessité d'un calcul certifié par ordinateur pourrait être un atout dans la recherche d'autres résultats de complexité autour de l'algorithme du simplexe.Les assistants de preuve sont les outils privilégiés à la certification de programmes et àla formalisation des mathématiques. Ils sont basés sur des langages de programmation permettant de définir des types de données haut-niveau, afin qu'ils puissent être manipulés pourobtenir des termes de preuves. Cependant, ces mêmes types de données s'avèrent inefficacesquand ils doivent servir au calcul numérique. On leur préfèrera des types de données plusproche d'une représentation machine. Résoudre la question du calcul numérique au sein des assistants de preuve nécessite de resoudre le problème de la gestion de l'équivalence entre ces différentes représentations de même données.L'objet de cette thèse est d'étudier la place du calcul numérique au sein des assistants depreuves, en implémentant en Coq un algorithme de certification de la structure d'un polytope,l'objet géométrique sous-jacent à l'exécution de l'algorithme du simplexe. En implémentantdeux versions de ce même algorithme, manipulant d'un côté des données haut-niveau et del'autre des données bas-niveau, nous mettons en place une méthodologie de raffinement de don-nées et de preuve d'équivalence entre les deux programmes. Les deux versions sont donc prouvées équivalentes à l'aide de cette méthodologie, et servent chacune leur propos. La versionbas-niveau est exécutée directement en Coq et effectue donc des calculs numériques. La version haut-niveau est prouvée correcte, et donc sa valeur de sortie peut servir d'hypothèse dansla rédaction d'autres preuves. Pour illustrer ce fonctionnement, nous produisons une preuveformelle de la réfutation de la conjecture de Hirsch, en confiant les calculs à l'algorithme bas-niveau et en interprétant les résultats obtenus grâce à l'algorithme haut-niveau.Néanmoins, les performances de l'algorithme bas-niveau, dédié aux calculs numériques, souffrent la comparaison avec les solutions informelles ayant le même but. Un autre objectif de ce travail de thèse est d'interpréter et de proposer des solutions pour améliorer ces résultats de performances. Nous avons identifié que l'arithmétique des rationnels constitue une véritable limitation lors de l'exécution de l'algorithme. Alors, nous proposons plusieurs solutions visant à limiter cet impact, de par un contrôle plus fin de la taille des coefficients calculés ou de la taille des fichiers manipulés. Notre solution la plus prometteuse vise à limiter le nombre d'opérations sur les rationnels en imitant la stratégie d'évaluation paresseuse, qui ne procède à un calcul uniquement lorsque celui-cin'a jamais été effectué préalablement.