Construction of real algebraic numbers in Coq - Archive ouverte HAL Access content directly
Conference Papers Year : 2012

Construction of real algebraic numbers in Coq

(1, 2, 3, 4)
1
2
3
4

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.
Fichier principal
Vignette du fichier
main.pdf (444.37 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-00671809 , version 1 (18-02-2012)
hal-00671809 , version 2 (13-06-2012)

Identifiers

  • HAL Id : hal-00671809 , version 2

Cite

Cyril Cohen. Construction of real algebraic numbers in Coq. ITP - 3rd International Conference on Interactive Theorem Proving - 2012, Aug 2012, Princeton, United States. ⟨hal-00671809v2⟩
688 View
1378 Download

Share

Gmail Facebook Twitter LinkedIn More