A Modular, Efficient Formalisation of Real Algebraic Numbers (CPP 2016)

Mon 18 - Tue 19 January 2016 St. Petersburg, Florida, United States

co-located with POPL 2016

Who

Wenda Li, Lawrence Paulson

Track

CPP 2016

Time Zone

The program is currently displayed in (GMT-05:00) Guadalajara, Mexico City, Monterrey.

Use conference time zone: (GMT-05:00) Guadalajara, Mexico City, MonterreySelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

Mon 18 Jan 2016 16:00 - 16:30 at Room St Petersburg II - Session 4: Mathematics

Abstract

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.

Wenda Li

University of Cambridge

China

Lawrence Paulson

Cambridge University