Contributions à la certification des calculs dans R : théorie, preuves, programmation

The Coq system is a proof assistant based on the Calculus of InductiveConstructions. In this work, we propose to enhance the automation of this system byproviding a reflexive and complete decision procedure for the firstorder theory of real numbers. The Type Theory implemented by the Coq system comprises atyped functional programming language, which we have used toimplement a Cylindrical Algebraic Decomposition algorithm (CAD). Thisalgorithm computes a partition of the space into sign-invariant,semi-algebraic cells for the polynomials of a given family. Hence itallows to decide all the formulae of this theory. Then we have to prove formally the correctness of the algorithm and of therelated decision procedure, using the Coq proof assistant. This work includes a library for certified polynomial arithmetic anda significant part of the formal proof of correctness of the sub-resultantsalgorithm. This last algorithm allows to compute efficiently thegreatest common divisor of polynomials with coefficients in a ring,and in particular of multivariate polynomials. We also propose a reflexive tactic for deciding equalities in ringand semi-ring structures, which enhances the performances of the toolpreviously available in the system by taking benefit of thecomputational abilities of the system. In a last part, we study the computational content of a constructiveproof of an elementary lemma of real analysis, called principle ofopen induction.Le logiciel Coq est un assistant à la preuve basé sur le Calcul desConstructions Inductives. Dans cette thèse nous proposons d'améliorer l'automatisation de ce système en le dotant d'une procédure de décision réflexive et complètepour la théorie du premier ordre de l'arithmétique réelle. La théorie des types implémentée par le système Coq comprend unlangage fonctionnel typé dans lequel nous avons programmé unalgorithme de Décomposition Algébrique Cylindrique (CAD). Cetalgorithme calcule une partition de l'espace en cellulessemi-algébriques sur lesquelles tous les polynômes d'une famille donnée ont un signe constant et permet ainsi de décider les formules de cette théorie. Il s'agit ensuite de prouver la correction de l'algorithme et de laprocédure de décision associée avec l'assistant à la preuve Coq. Ce travail comprend en particulier une librairie d'arithmétique polynomialecertifiée et une partie significative de la preuve formelle de correction del'algorithme des sous-résultants. Ce dernier algorithme permet de calculerefficacement le plus grand commun diviseur de polynômes à coefficients dans unanneau, en particulier à plusieurs variables. Nous proposons également une tactique réflexive de décision des égalités dans lesstructures d'anneau et de semi-anneaux qui améliore les performances de l'outildéjà disponible et augmente son spectre d'action en exploitant les possibilités decalcul du système. Dans une dernière partie, nous étudions le contenu calculatoire d'une preuveconstructive d'un lemme élémentaire d'analyse réelle, le principe d'inductionouverte