Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Construction of real algebraic numbers in Coq

Cyril Cohen 1, 2, 3
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.
Document type :
Preprints, Working Papers, ...
Complete list of metadatas
Contributor : Cyril Cohen <>
Submitted on : Saturday, February 18, 2012 - 8:08:55 PM
Last modification on : Wednesday, March 27, 2019 - 4:41:28 PM
Long-term archiving on: : Friday, November 23, 2012 - 1:40:16 PM


Files produced by the author(s)


  • HAL Id : hal-00671809, version 1


Cyril Cohen. Construction of real algebraic numbers in Coq. 2012. ⟨hal-00671809v1⟩



Record views


Files downloads