Skip to Content

A verified implementation of algebraic numbers in Isabelle/HOL

Posted on

Authors:

  • Joosten, Sebastiaan J.
  • Thiemann, René
  • Yamada, Akihisa

Published in: Journal of automated reasoning pp 363–389

Paper

Abstract:

We formalize algebraic numbers in Isabelle/HOL. Our development serves as a verified implementation of algebraic operations on real and complex numbers. We moreover provide algorithms that can identify all the real or complex roots of rational polynomials, and two implementations to display algebraic numbers, an approximative version and an injective precise one. We obtain verified Haskell code for these operations via Isabelle’s code generator. The development combines various existing formalizations such as matrices, Sturm’s theorem, and polynomial factorization, and it includes new formalizations about bivariate polynomials, unique factorization domains, resultants and subresultants.

BibTeX entry:

@article{Joosten20,
 abstract = {We formalize algebraic numbers in Isabelle/HOL. Our development serves as a verified implementation of algebraic operations on real and complex numbers. We moreover provide algorithms that can identify all the real or complex roots of rational polynomials, and two implementations to display algebraic numbers, an approximative version and an injective precise one. We obtain verified Haskell code for these operations via Isabelle's code generator. The development combines various existing formalizations such as matrices, Sturm's theorem, and polynomial factorization, and it includes new formalizations about bivariate polynomials, unique factorization domains, resultants and subresultants.},
 author = {Joosten, Sebastiaan JC and Thiemann, Ren{\'e} and Yamada, Akihisa},
 date-added = {2021-09-18 14:47:12 -0400},
 date-modified = {2021-09-18 15:29:29 -0400},
 journal = {Journal of automated reasoning},
 month = {June},
 number = {3},
 pages = {363--389},
 publisher = {Springer Netherlands},
 title = {A verified implementation of algebraic numbers in Isabelle/HOL},
 volume = {64},
 year = {2020}
}