Construction of Real Algebraic Numbers in Coq

DOI10.1007/978-3-642-32347-8_6zbMath1360.68744OpenAlexW2134124371MaRDI QIDQ2914733

Cyril Cohen

Publication date: 20 September 2012

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-32347-8_6

Mathematics Subject Classification ID

Related Items (11)

Unnamed Item ⋮ Unnamed Item ⋮ Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL ⋮ Formal proofs of rounding error bounds. With application to an automatic positive definiteness check ⋮ A certifying square root and division elimination ⋮ A verified implementation of algebraic numbers in Isabelle/HOL ⋮ Algebraic Numbers in Isabelle/HOL ⋮ Classification of finite fields with applications ⋮ Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers ⋮ A formalization of Dedekind domains and class groups of global fields ⋮ Flexible proof production in an industrial-strength SMT solver

Uses Software

• Coq

This page was built for publication: Construction of Real Algebraic Numbers in Coq