Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal

Many problems in computer algebra and numerical analysis can be reduced to counting or approximating the real roots of a polynomial within an interval. Existing verified root-counting procedures in major proof assistants are mainly based on the classical Sturm theorem, which only counts distinct roots.

In this paper, we have strengthened the root-counting ability in Isabelle/HOL by first formally proving the Budan-Fourier theorem. Subsequently, based on Descartes’ rule of signs and Taylor shift, we have provided a verified procedure to efficiently over-approximate the number of real roots within an interval, counting multiplicity. For counting multiple roots exactly, we have extended our previous formalisation of Sturm’s theorem. Finally, as an application, we apply the results above to improve our previous certified complex-root-counting procedures based on Cauchy indices. We believe those verified routines will be crucial for certifying programs and building tactics.

Mon 14 Jan

16:00 - 17:30: CPP 2019 - Research Papers: Formalization of Mathematics and Computer Algebra at Sala XII
Chair(s): Georges GonthierInria
CPP-201916:00 - 16:30
Research paper
Robert Y. LewisVrije Universiteit Amsterdam
CPP-201916:30 - 17:00
Research paper
Wenda LiUniversity of Cambridge, Lawrence PaulsonUniversity of Cambridge
CPP-201917:00 - 17:30
Research paper