Si la communauté internationale de géométrie algorithmique a souvent<br />la tentation de s'engouffrer dans des recherches essentiellement<br />théoriques, et en particulier combinatoires, la grande originalité des<br />travaux à l'INRIA résidait déjà à l'époque de mes débuts dans le<br />souci de leur validation expérimentale et de leur applicabilité. <br /><br />Le domaine a suivi globalement une évolution dans cette direction,<br />en particulier grâce à l'``Impact Task Force Report''. Notre intérêt pour le transfert technologique et<br />industriel, ainsi que pour l'établissement d'une plateforme pour la<br />recherche, a pris pendant ce temps une tournure encore plus concrète<br />avec notre implication très forte dans le projet CGAL<br />dont notre équipe est l'un des moteurs.<br /><br />Ce document prend le parti de présenter les travaux sous l'angle de<br />cette préoccupation pratique.<br />Il comporte deux chapitres principaux : le premier rassemble<br />des travaux sur les triangulations, le second présente des travaux sur<br />les objets courbes. Ces deux chapitres se concluent par un ensemble de<br />directions ouvertes. Le troisième chapitre survole rapidement d'autres<br />résultats.

Cette thèse se rattache à l'algèbre linéaire formelle. Elle est composée de deux parties: la première, consacrée à l'étude des formes normales de matrices, constitue un ensemble d'outils utilisés dans la seconde qui, pour sa part, présente des méthodes matricielles de résolution de deux types de systèmes différentiels: les systèmes différentiels à coefficients constants et les systèmes différentiels ayant un point singulier régulier isolé. Dans la première partie, nous avons étudié, implémentés dans le système de calcul formel AXIOM, et comparés tant de manière théorique qu'expérimentale des algorithmes de calcul de diverses formes normales (Frobenius, Smith, Jordan) de matrices à coefficients rationnels. Dans la seconde, nous avons montré quels sont les avantages et les inconvénients de l'utilisation de ces algorithmes pour trois applications: le calcul de l'exponentielle d'une matrice, la résolution d'équations matricielles et la résolution matricielle de systèmes différentiels ayant une singularité régulière isolée. En particulier, nous avons abordé le problème épineux de la manipulation des nombres algébriques apparaissant nécessairement lorsque l'on calcule formellement, la forme de Jordan d'une matrice à coefficients rationnels

On décrit et on étudie une matrice Q inversible telle que Q F = JQ ou J est la forme normale de Jordan d'une matrice carrée A, et F sa forme de Frobenius. On propose un algorithme efficace pour le calcul de l'inverse de Q et deux algorithmes donnant la forme de Frobenius d'une matrice n x n quelconque. Dans le cas ou les éléments de A sont des nombres rationnels, on montre que la complexité de l'un des algorithmes est polynomiale. On considère aussi le cas des matrices A coefficients dans le corps des nombres algébriques sur Q

Cette thèse présente une formalisation des nombres algébriques et de leur théorie. Elle apporte deux nouvelles contributions importantes à la formalisation de résultats mathématiques dans des assistants à la preuve, ici Coq : la construction intuitionniste des nombres algébriques réels et la preuve qu'ils constituent un corps réel clos, ainsi que la programmation et la certification de procédures d'élimination des quantificateurs pour les théories des corps algébriquement clos et des corps réels clos. Pour atteindre ces résultats, nous avons apporté des contributions aux outils et aux méthodologies de preuves et de formalisation des mathématiques en Coq. En particulier, nous fournissons pour Coq/SSReflect un cadre pour travailler avec des types quotients. Nous fournissons une bibliothèque complète sur les structures algébriques de nombres ordonnés et normés. Nous avons réalisé une courte implémentation des réels de Cauchy accompagnée de tactiques pour effectuer facilement des raisonnements comportant des affirmations de la forme "soit n un entier suffisamment grand", couramment utilisés dans les preuves mathématiques sur papier. Nous avons également développé une petite bibliothèque d'analyse de base sur les polynômes à coefficients dans un corps réel clos. Une grande partie de nos résultats s'intègrent dans la formalisation de la preuve du théorème de Feit-Thompson et ont aussi pour objectif d'aider à certifier des procédures plus efficace d'élimination des quantificateurs sur les réels.

Un problème de géométrie algébrique réelle s'exprime sous forme d’un système d’équations et d’inéquations polynomiales, dont l’ensemble des solutions est un ensemble semi-algébrique. L'objectif de cette thèse est de montrer comment les algorithmes de ce domaine peuvent être décrits formellement dans le langage du système de preuve Coq.Un premier résultat est la définition formelle et la certification de l’algorithme de transformation de Newton présentée dans la thèse d'A. Bostan. Ce travail fait intervenir non seulement des polynômes, mais également des séries formelles tronquées. Un deuxième résultat est la description d'un type de donnée représentant les ensembles semi-algébriques. Un ensemble semialgébrique est représenté par une formule logique du premier ordre basée sur des comparaisons entre expressions polynomiales multivariées. Pour ce type de données, nous montrons comment obtenir les différentes opérations ensemblistes et allons jusqu'à décrire les fonctions semi-algébriques. Pour toutes ces étapes, nous fournissons des preuves formelles vérifiées à l'aide de Coq. Enfin, nous montrons également comment la continuité des fonctions semi-algébrique peut être décrite, mais sans en fournir une preuve formelle complète. / A real algebraic geometry problem is expressed as a system of polynomial equations and inequalities, and the set of solutions are semi-algebraic sets. The objective of this thesis is to show how the algorithms of this domain can be formally described in the language of the Coq proof system. A first result is the formal definition and certification of the Newton transformation algorithm presented in A. Bostan's thesis. This work involves not only polynomials, but also truncated formal series. A second result is the description of a data type representing semi-algebraic sets. A semi-algebraic set is represented by a first-order logical formula based on comparisons between multivariate polynomial expressions. For this type of data, we show how to obtain the different set operations all the way to describing semialgebraic functions. For all these steps, we provide formal proofs verified with Coq. Finally, we also show how the continuity of semi-algebraic functions can be described, but without providing a fully formalized proof.