Construction des nombres algébriques réels en Coq

Cyril Cohen 1, 2, 3, 4
3 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
Résumé : Cet article présente une construction en Coq de l'ensemble des nombres algébriques réels, ainsi qu'une preuve formelle que cet ensemble est muni d'une structure de corps réel clos discret archimédien. Cette construction vient ainsi implémenter une interface de corps réel clos réalisée dans un travail antérieur et bénéficie alors de la propriété d'élimination des quantificateurs, formellement prouvée pour toute instance de l'interface. Ce travail est destiné à servir de fondement à une construction de l'ensemble des nombres algébriques complexes, ainsi que d'implémentation de référence pour la certification des nombreux algorithmes de calcul formel qui utilisent des nombres algébriques.
Type de document :
Communication dans un congrès
JFLA - Journées Francophones des Langages Applicatifs - 2012, Feb 2012, Carnac, France. 2012
Liste complète des métadonnées

https://hal.inria.fr/hal-00665965
Contributeur : Alain Monteil <>
Soumis le : vendredi 3 février 2012 - 12:03:19
Dernière modification le : jeudi 9 février 2017 - 15:06:58
Document(s) archivé(s) le : mercredi 14 décembre 2016 - 04:02:24

Fichier

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

Identifiants

  • HAL Id : hal-00665965, version 1

Collections

Citation

Cyril Cohen. Construction des nombres algébriques réels en Coq. JFLA - Journées Francophones des Langages Applicatifs - 2012, Feb 2012, Carnac, France. 2012. <hal-00665965>

Partager

Métriques

Consultations de
la notice

294

Téléchargements du document

248