{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:14:58Z","timestamp":1750306498333,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":13,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,1,18]],"date-time":"2016-01-18T00:00:00Z","timestamp":1453075200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,1,18]]},"DOI":"10.1145\/2854065.2854074","type":"proceedings-article","created":{"date-parts":[[2016,1,12]],"date-time":"2016-01-12T13:18:57Z","timestamp":1452604737000},"page":"66-75","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["A modular, efficient formalisation of real algebraic numbers"],"prefix":"10.1145","author":[{"given":"Wenda","family":"Li","sequence":"first","affiliation":[{"name":"University of Cambridge, UK"}]},{"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}]}],"member":"320","published-online":{"date-parts":[[2016,1,18]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-33099-2","volume-title":"Algorithms in Real Algebraic Geometry (Algorithms and Computation in Mathematics)","author":"Basu S.","year":"2006","unstructured":"S. Basu , R. Pollack , and M.-F. Roy . Algorithms in Real Algebraic Geometry (Algorithms and Computation in Mathematics) . Springer-Verlag New York, Inc. , Secaucus, NJ, USA , 2006 . ISBN 3540330984. S. Basu, R. Pollack, and M.-F. Roy. Algorithms in Real Algebraic Geometry (Algorithms and Computation in Mathematics). Springer-Verlag New York, Inc., Secaucus, NJ, USA, 2006. ISBN 3540330984."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_12"},{"key":"e_1_3_2_1_4_1","first-page":"2150","author":"Divas\u00f3n J.","year":"2013","unstructured":"J. Divas\u00f3n and J. Aransay . Rank-Nullity Theorem in Linear Algebra. Archive of Formal Proofs , Jan. 2013 . ISSN 2150 - 2914 x. http:\/\/afp. sf.net\/entries\/Rank_Nullity_Theorem.shtml, Formal proof development. J. Divas\u00f3n and J. Aransay. Rank-Nullity Theorem in Linear Algebra. Archive of Formal Proofs, Jan. 2013. ISSN 2150-914x. http:\/\/afp. sf.net\/entries\/Rank_Nullity_Theorem.shtml, Formal proof development.","journal-title":"Rank-Nullity Theorem in Linear Algebra. Archive of Formal Proofs"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_14"},{"key":"e_1_3_2_1_6_1","volume-title":"Code generation from Isabelle\/HOL theories","author":"Haftmann F.","year":"2015","unstructured":"F. Haftmann and L. Bulwahn . Code generation from Isabelle\/HOL theories . 2015 . URL https:\/\/isabelle.in.tum.de\/dist\/ Isabelle 2015\/doc\/codegen.pdf. F. Haftmann and L. Bulwahn. Code generation from Isabelle\/HOL theories. 2015. URL https:\/\/isabelle.in.tum.de\/dist\/ Isabelle2015\/doc\/codegen.pdf."},{"key":"e_1_3_2_1_7_1","unstructured":"F. Haftmann A. Lochbihler and R. Wolfgang Schreiner. Towards abstract and executable multivariate polynomials in isabelle.  F. Haftmann A. Lochbihler and R. Wolfgang Schreiner. Towards abstract and executable multivariate polynomials in isabelle."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_9"},{"key":"e_1_3_2_1_10_1","first-page":"2150","article-title":"The Sturm-Tarski Theorem","author":"Li W.","year":"2014","unstructured":"W. Li . The Sturm-Tarski Theorem . Archive of Formal Proofs , Sept. 2014 . ISSN 2150 - 2914 x. http:\/\/afp.sf.net\/entries\/Sturm_ Tarski.shtml, Formal proof development. W. Li. The Sturm-Tarski Theorem. Archive of Formal Proofs, Sept. 2014. ISSN 2150-914x. http:\/\/afp.sf.net\/entries\/Sturm_ Tarski.shtml, Formal proof development.","journal-title":"Archive of Formal Proofs"},{"key":"e_1_3_2_1_11_1","volume-title":"A complete decision procedure for univariate polynomial problems in Isabelle\/HOL. arXiv preprint arXiv:1506.08238","author":"Li W.","year":"2015","unstructured":"W. Li , G. O. Passmore , and L. C. Paulson . A complete decision procedure for univariate polynomial problems in Isabelle\/HOL. arXiv preprint arXiv:1506.08238 , 2015 . W. Li, G. O. Passmore, and L. C. Paulson. A complete decision procedure for univariate polynomial problems in Isabelle\/HOL. arXiv preprint arXiv:1506.08238, 2015."},{"key":"e_1_3_2_1_12_1","volume-title":"Programming TLS in Isabelle\/HOL. In Isabelle Workshop","volume":"2014","author":"Lochbihler A.","year":"2014","unstructured":"A. Lochbihler and M. Z\u00fcst . Programming TLS in Isabelle\/HOL. In Isabelle Workshop , volume 2014 , 2014 . A. Lochbihler and M. Z\u00fcst. Programming TLS in Isabelle\/HOL. In Isabelle Workshop, volume 2014, 2014."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"Nipkow T.","year":"2002","unstructured":"T. Nipkow , L. C. Paulson , and M. Wenzel . Isabelle\/HOL: A Proof Assistant for Higher-Order Logic . Springer , 2002 . T. Nipkow, L. C. Paulson, and M. Wenzel. Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer, 2002."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31374-5_24"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2006.06.004"}],"event":{"name":"CPP 2016: Certified Proofs and Programs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"St. Petersburg FL USA","acronym":"CPP 2016"},"container-title":["Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2854065.2854074","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2854065.2854074","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:48:47Z","timestamp":1750225727000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2854065.2854074"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1,18]]},"references-count":13,"alternative-id":["10.1145\/2854065.2854074","10.1145\/2854065"],"URL":"https:\/\/doi.org\/10.1145\/2854065.2854074","relation":{},"subject":[],"published":{"date-parts":[[2016,1,18]]},"assertion":[{"value":"2016-01-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}