{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:30:40Z","timestamp":1750221040602,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":32,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,1,14]],"date-time":"2019-01-14T00:00:00Z","timestamp":1547424000000},"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":[[2019,1,14]]},"DOI":"10.1145\/3293880.3294092","type":"proceedings-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:56Z","timestamp":1546608836000},"page":"52-64","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Counting polynomial roots in Isabelle\/HOL: a formal proof of the Budan-Fourier theorem"],"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":[[2019,1,14]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"crossref","first-page":"89","DOI":"10.55630\/sjc.2008.2.89-104","article-title":"On the various bisection methods derived from Vincent\u2019s theorem","volume":"2","author":"Akritas Alkiviadis","year":"2008","unstructured":"Alkiviadis Akritas , Adam Strzebo\u0144ski , and Panagiotis Vigklas . 2008 . On the various bisection methods derived from Vincent\u2019s theorem . Serdica Journal of Computing 2 , 1 (2008), 89 \u2013 104 . Alkiviadis Akritas, Adam Strzebo\u0144ski, and Panagiotis Vigklas. 2008. On the various bisection methods derived from Vincent\u2019s theorem. Serdica Journal of Computing 2, 1 (2008), 89\u2013104.","journal-title":"Serdica Journal of Computing"},{"volume-title":"Method. In Computer Algebra in Education","author":"Akritas Alkiviadis G","key":"e_1_3_2_1_2_1","unstructured":"Alkiviadis G Akritas . 2008. There is no Descartes \u2019 Method. In Computer Algebra in Education , M.J. Wester and M. Beaudin (Eds.). AulonaPress, 19\u201335. On the Internet at https:\/\/faculty.e-ce.uth.gr\/akritas\/articles\/ 71.pdf . Alkiviadis G Akritas. 2008. There is no Descartes\u2019 Method. In Computer Algebra in Education, M.J. Wester and M. Beaudin (Eds.). AulonaPress, 19\u201335. On the Internet at https:\/\/faculty.e-ce.uth.gr\/akritas\/articles\/ 71.pdf ."},{"volume-title":"Ordinary Differential Equations","author":"Arnold Vladimir I","key":"e_1_3_2_1_3_1","unstructured":"Vladimir I Arnold . 1992. Ordinary Differential Equations . Springer . Vladimir I Arnold. 1992. Ordinary Differential Equations. Springer."},{"key":"e_1_3_2_1_4_1","unstructured":"R. D. Arthan. 2007. Descartes\u2019 Rule of Signs by an Easy Induction. Online at https:\/\/arxiv.org\/abs\/0710.1881 .  R. D. Arthan. 2007. Descartes\u2019 Rule of Signs by an Easy Induction. Online at https:\/\/arxiv.org\/abs\/0710.1881 ."},{"volume-title":"Algorithms in Real Algebraic Geometry. Algorithms and Computation in Mathematics","author":"Basu Saugata","key":"e_1_3_2_1_5_1","unstructured":"Saugata Basu , Richard Pollack , and Marie-Franco \u00b8ise Roy . 2006. Algorithms in Real Algebraic Geometry. Algorithms and Computation in Mathematics , Vol. 10 . Springer . Saugata Basu, Richard Pollack, and Marie-Franco \u00b8ise Roy. 2006. Algorithms in Real Algebraic Geometry. Algorithms and Computation in Mathematics, Vol. 10. Springer."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000090"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32347-8_6"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/800205.806346"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.2002.0547"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/143242.143308"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676724.2693166"},{"key":"e_1_3_2_1_12_1","volume-title":"Rule of Signs. Archive of Formal Proofs (Dec.","author":"Eberl Manuel","year":"2015","unstructured":"Manuel Eberl . 2015. Descartes \u2019 Rule of Signs. Archive of Formal Proofs (Dec. 2015 ). http:\/\/isa-afp.org\/entries\/Descartes_Sign_Rule. html , Formal proof development. Manuel Eberl. 2015. Descartes\u2019 Rule of Signs. Archive of Formal Proofs (Dec. 2015). http:\/\/isa-afp.org\/entries\/Descartes_Sign_Rule. html , Formal proof development."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2930889.2930937"},{"key":"e_1_3_2_1_15_1","volume-title":"The Sturm-Tarski Theorem. Archive of Formal Proofs (Sept","author":"Wenda Li.","year":"2014","unstructured":"Wenda Li. 2014. The Sturm-Tarski Theorem. Archive of Formal Proofs (Sept . 2014 ). Wenda Li. 2014. The Sturm-Tarski Theorem. Archive of Formal Proofs (Sept. 2014)."},{"key":"e_1_3_2_1_16_1","volume-title":"Count the Number of Complex Roots. Archive of Formal Proofs (Oct","author":"Wenda Li.","year":"2017","unstructured":"Wenda Li. 2017. Count the Number of Complex Roots. Archive of Formal Proofs (Oct . 2017 ). Wenda Li. 2017. Count the Number of Complex Roots. Archive of Formal Proofs (Oct. 2017)."},{"key":"e_1_3_2_1_17_1","volume-title":"The Budan-Fourier Theorem and Counting Real Roots with Multiplicity. Archive of Formal Proofs (Sept","author":"Wenda Li.","year":"2018","unstructured":"Wenda Li. 2018. The Budan-Fourier Theorem and Counting Real Roots with Multiplicity. Archive of Formal Proofs (Sept . 2018 ). Wenda Li. 2018. The Budan-Fourier Theorem and Counting Real Roots with Multiplicity. Archive of Formal Proofs (Sept. 2018)."},{"key":"e_1_3_2_1_18_1","first-page":"3","article-title":"Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle\/HOL","volume":"44","author":"Li Wenda","year":"2017","unstructured":"Wenda Li , Grant Olney Passmore , and Lawrence C Paulson . 2017 . Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle\/HOL . Journal of Automated Reasoning 44 , 3 (Aug. 2017), 175\u201323. Wenda Li, Grant Olney Passmore, and Lawrence C Paulson. 2017. Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle\/HOL. Journal of Automated Reasoning 44, 3 (Aug. 2017), 175\u201323.","journal-title":"Journal of Automated Reasoning"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854074"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-43144-4_15"},{"key":"e_1_3_2_1_21_1","volume-title":"Evaluating Winding Numbers and Counting Complex Roots through Cauchy Indices in Isabelle\/HOL. CoRR abs\/1804.03922","author":"Li Wenda","year":"2018","unstructured":"Wenda Li and Lawrence C Paulson . 2018. Evaluating Winding Numbers and Counting Complex Roots through Cauchy Indices in Isabelle\/HOL. CoRR abs\/1804.03922 ( 2018 ). Wenda Li and Lawrence C Paulson. 2018. Evaluating Winding Numbers and Counting Complex Roots through Cauchy Indices in Isabelle\/HOL. CoRR abs\/1804.03922 (2018)."},{"key":"e_1_3_2_1_22_1","volume-title":"Formal Proofs in Real Algebraic Geometry: from Ordered Fields to Quantifier Elimination. Logical Methods in Computer Science 8, 1","author":"Mahboubi Assia","year":"2012","unstructured":"Assia Mahboubi and Cyril Cohen . 2012. Formal Proofs in Real Algebraic Geometry: from Ordered Fields to Quantifier Elimination. Logical Methods in Computer Science 8, 1 ( 2012 ). Assia Mahboubi and Cyril Cohen. 2012. Formal Proofs in Real Algebraic Geometry: from Ordered Fields to Quantifier Elimination. Logical Methods in Computer Science 8, 1 (2012)."},{"volume-title":"Geometry of Polynomials","author":"Marden Morris","key":"e_1_3_2_1_23_1","unstructured":"Morris Marden . 1949. Geometry of Polynomials . Second Edition. American Mathematical Society, Providence, Rhode Island . Morris Marden. 1949. Geometry of Polynomials. Second Edition. American Mathematical Society, Providence, Rhode Island."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_22"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9320-x"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541"},{"volume-title":"Analytic Theory of Polynomials","author":"Rahman Qazi Ibadur","key":"e_1_3_2_1_27_1","unstructured":"Qazi Ibadur Rahman and Gerhard Schmeisser . 2002. Analytic Theory of Polynomials . Oxford University Press . Qazi Ibadur Rahman and Gerhard Schmeisser. 2002. Analytic Theory of Polynomials. Oxford University Press."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.cam.2003.08.015"},{"key":"e_1_3_2_1_29_1","volume-title":"Algebraic Numbers in Isabelle\/HOL. In 7th International Conference on Interactive Theorem Proving, ITP","author":"Thiemann Ren\u00e9","year":"2016","unstructured":"Ren\u00e9 Thiemann and Akihisa Yamada . 2016 . Algebraic Numbers in Isabelle\/HOL. In 7th International Conference on Interactive Theorem Proving, ITP 2016, Jasmin Christian Blanchette and Stephan Merz (Eds.). Springer, 391\u2013408. Ren\u00e9 Thiemann and Akihisa Yamada. 2016. Algebraic Numbers in Isabelle\/HOL. In 7th International Conference on Interactive Theorem Proving, ITP 2016, Jasmin Christian Blanchette and Stephan Merz (Eds.). Springer, 391\u2013408."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854073"},{"key":"e_1_3_2_1_31_1","volume-title":"Archive of Formal Proofs (Jan","author":"Thiemann Ren\u00e9","year":"2016","unstructured":"Ren\u00e9 Thiemann and Akihisa Yamada . 2016. Polynomial Factorization . Archive of Formal Proofs (Jan . 2016 ). http:\/\/isa-afp.org\/entries\/ Polynomial_Factorization.html , Formal proof development. Ren\u00e9 Thiemann and Akihisa Yamada. 2016. Polynomial Factorization. Archive of Formal Proofs (Jan. 2016). http:\/\/isa-afp.org\/entries\/ Polynomial_Factorization.html , Formal proof development."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/322077.322084"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993886.1993938"}],"event":{"name":"CPP '19: 8th ACM SIGPLAN International Conference on Certified Programs and Proofs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"Cascais Portugal","acronym":"CPP '19"},"container-title":["Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3293880.3294092","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3293880.3294092","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:43:50Z","timestamp":1750207430000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3293880.3294092"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,14]]},"references-count":32,"alternative-id":["10.1145\/3293880.3294092","10.1145\/3293880"],"URL":"https:\/\/doi.org\/10.1145\/3293880.3294092","relation":{},"subject":[],"published":{"date-parts":[[2019,1,14]]},"assertion":[{"value":"2019-01-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}