Show simple item record

dc.contributor.authorLi, Wendaen
dc.contributor.authorPaulson, Lawrenceen
dc.date.accessioned2016-02-11T10:53:31Z
dc.date.available2016-02-11T10:53:31Z
dc.date.issued2016-01-18en
dc.identifier.citationLi et al. CPP 2016 Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (2016) pp. 66-75. doi: 10.1145/2854065.2854074en
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/253716
dc.description.abstractThis 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.sponsorshipThe CSC Cambridge International Scholarship is generously funding Wenda Li’s Ph.D. course.
dc.languageEnglishen
dc.language.isoenen
dc.publisherAssociation for Computing Machinery
dc.subjectreal algebraic geometryen
dc.subjectIsabelle/HOLen
dc.subjectdecision procedureen
dc.titleA modular, efficient formalisation of real algebraic numbersen
dc.typeConference Object
dc.description.versionThis is the author accepted manuscript. The final version is available from the Association for Computing Machinery via http://dx.doi.org/10.1145/2854065.2854074en
prism.endingPage75
prism.publicationDate2016en
prism.publicationNameCPP 2016 Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofsen
prism.startingPage66
rioxxterms.versionofrecord10.1145/2854065.2854074en
rioxxterms.licenseref.urihttp://www.rioxx.net/licenses/all-rights-reserveden
rioxxterms.licenseref.startdate2016-01-18en
dc.contributor.orcidPaulson, Lawrence [0000-0003-0288-4279]
rioxxterms.typeConference Paper/Proceeding/Abstracten
pubs.funder-project-idEPSRC (EP/I011005/1)


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record