Formalizing real analysis for polynomials

Cyril Cohen 1, 2, 3
1 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : When reasoning formally with polynomials over real numbers, or more generally real closed fields, we need to be able to manipulate easily statements featuring an order relation, either in their conditions or in their conclusion. For instance, we need to state the intermediate value theorem and the mean value theorem and we need tools to ease both their proof and their further use. For that purpose we propose a Coq library for ordered integral domains and ordered fields with decidable comparison. In this paper we present the design choices of this libraries, and show how it has been used as a basis for developing a fare amount of basic real algebraic geometry.
Type de document :
Pré-publication, Document de travail
2010
Liste complète des métadonnées


https://hal.inria.fr/inria-00545778
Contributeur : Cyril Cohen <>
Soumis le : dimanche 12 décembre 2010 - 17:27:44
Dernière modification le : vendredi 10 février 2017 - 01:12:52
Document(s) archivé(s) le : vendredi 2 décembre 2016 - 18:17:39

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00545778, version 1

Collections

Citation

Cyril Cohen. Formalizing real analysis for polynomials. 2010. <inria-00545778>

Partager

Métriques

Consultations de
la notice

252

Téléchargements du document

219