Skip to Main content Skip to Navigation
Conference papers

Construction of real algebraic numbers in Coq

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 :
Conference papers
Complete list of metadata

Cited literature [13 references]  Display  Hide  Download
Contributor : Cyril Cohen Connect in order to contact the contributor
Submitted on : Wednesday, June 13, 2012 - 11:24:43 PM
Last modification on : Thursday, January 20, 2022 - 5:26:33 PM
Long-term archiving on: : Thursday, December 15, 2016 - 2:29:18 PM


Files produced by the author(s)


  • HAL Id : hal-00671809, version 2



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⟩



Les métriques sont temporairement indisponibles