CPP 2016
Mon 18 - Tue 19 January 2016 St. Petersburg, Florida, United States
co-located with POPL 2016
Mon 18 Jan 2016 16:00 - 16:30 at Room St Petersburg II - Session 4: Mathematics

This paper shows a construction of 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 at 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.

Mon 18 Jan

Displayed time zone: Guadalajara, Mexico City, Monterrey change