A modular, efficient formalisation of real algebraic numbers
CPP 2016 Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs
Association for Computing Machinery
MetadataShow full item record
Li, W., & Paulson, L. (2016). A modular, efficient formalisation of real algebraic numbers. CPP 2016 Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 66-75. https://doi.org/10.1145/2854065.2854074
This paper presents a construction of the real algebraic numbers with executable arithmetic operations in Isabelle/HOL. Instead of verified resultants, arithmetic operations on real algebraic numbers are based on a decision procedure to decide the sign of a bivariate polynomial (with rational coefficients) at a real algebraic point. The modular design allows the safe use of fast external code. This work can be the basis for decision procedures that rely on real algebraic numbers.
real algebraic geometry, Isabelle/HOL, decision procedure
The CSC Cambridge International Scholarship is generously funding Wenda Li’s Ph.D. course.
External DOI: https://doi.org/10.1145/2854065.2854074
This record's URL: https://www.repository.cam.ac.uk/handle/1810/253716