A modular, efficient formalisation of real algebraic numbers
| dc.contributor.author | Li, Wenda | en |
| dc.contributor.author | Paulson, Lawrence | en |
| dc.date.accessioned | 2016-02-11T10:53:31Z | |
| dc.date.available | 2016-02-11T10:53:31Z | |
| dc.date.issued | 2016-01-18 | en |
| dc.identifier.citation | Li et al. CPP 2016 Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (2016) pp. 66-75. doi: 10.1145/2854065.2854074 | en |
| dc.identifier.uri | https://www.repository.cam.ac.uk/handle/1810/253716 | |
| dc.description.abstract | 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. | |
| dc.description.sponsorship | The CSC Cambridge International Scholarship is generously funding Wenda Li’s Ph.D. course. | |
| dc.language | English | en |
| dc.language.iso | en | en |
| dc.publisher | Association for Computing Machinery | |
| dc.subject | real algebraic geometry | en |
| dc.subject | Isabelle/HOL | en |
| dc.subject | decision procedure | en |
| dc.title | A modular, efficient formalisation of real algebraic numbers | en |
| dc.type | Conference Object | |
| dc.description.version | This is the author accepted manuscript. The final version is available from the Association for Computing Machinery via http://dx.doi.org/10.1145/2854065.2854074 | en |
| prism.endingPage | 75 | |
| prism.publicationDate | 2016 | en |
| prism.publicationName | CPP 2016 Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs | en |
| prism.startingPage | 66 | |
| rioxxterms.versionofrecord | 10.1145/2854065.2854074 | en |
| rioxxterms.licenseref.uri | http://www.rioxx.net/licenses/all-rights-reserved | en |
| rioxxterms.licenseref.startdate | 2016-01-18 | en |
| dc.contributor.orcid | Paulson, Lawrence [0000-0003-0288-4279] | |
| rioxxterms.type | Conference Paper/Proceeding/Abstract | en |
| pubs.funder-project-id | EPSRC (EP/I011005/1) |
Files in this item
This item appears in the following Collection(s)
-
Scholarly Works - Computer Science and Technology
-
Symplectic mapped items for data match
This collection contains all articles, datasets and conference objects to be harvested