Construction of real algebraic numbers in Coq

Cyril Cohen 1, 2, 3, 4
3 TYPICAL - Types, Logic and computing
Inria Saclay - Ile de France, LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], CNRS - Centre National de la Recherche Scientifique : UMR, Polytechnique - X
Abstract : This paper shows a construction in Coq of the set of real algebraic numbers, together with a formal proof that this set has a structure of discrete archimedian real closed field. This construction hence implements an interface of real closed field. Instances of such an interface immediately enjoy quantifier elimination thanks to a previous work. This work also intends to be a basis for the construction of complex algebraic numbers and to be a reference implementation for the certification of numerous algorithms relying on algebraic numbers in computer algebra.
Type de document :
Communication dans un congrès
Lennart Beringer and Amy Felty. ITP - 3rd International Conference on Interactive Theorem Proving - 2012, Aug 2012, Princeton, United States. Springer, 2012


https://hal.inria.fr/hal-00671809
Contributeur : Cyril Cohen <>
Soumis le : mercredi 13 juin 2012 - 23:24:43
Dernière modification le : jeudi 9 février 2017 - 15:07:58
Document(s) archivé(s) le : jeudi 15 décembre 2016 - 14:29:18

Fichier

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

Identifiants

  • HAL Id : hal-00671809, version 2

Collections

Citation

Cyril Cohen. Construction of real algebraic numbers in Coq. Lennart Beringer and Amy Felty. ITP - 3rd International Conference on Interactive Theorem Proving - 2012, Aug 2012, Princeton, United States. Springer, 2012. <hal-00671809v2>

Partager

Métriques

Consultations de
la notice

374

Téléchargements du document

252