Construction des nombres algébriques réels en Coq

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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [11 references]  Display  Hide  Download

https://hal.inria.fr/hal-00665965
Contributor : Alain Monteil <>
Submitted on : Friday, February 3, 2012 - 12:03:19 PM
Last modification on : Wednesday, March 27, 2019 - 4:41:28 PM
Long-term archiving on : Wednesday, December 14, 2016 - 4:02:24 AM

File

paper_11.pdf
Files produced by the author(s)

Identifiers

  • 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. ⟨hal-00665965⟩

Share

Metrics

Record views

532

Files downloads

369