{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:36:15Z","timestamp":1740123375888,"version":"3.37.3"},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2018,12,9]],"date-time":"2018-12-09T00:00:00Z","timestamp":1544313600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"Austrian Science Fund","award":["Y757"],"award-info":[{"award-number":["Y757"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2020,3]]},"DOI":"10.1007\/s10817-018-09504-w","type":"journal-article","created":{"date-parts":[[2018,12,9]],"date-time":"2018-12-09T08:55:56Z","timestamp":1544345756000},"page":"363-389","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A Verified Implementation of Algebraic Numbers in Isabelle\/HOL"],"prefix":"10.1007","volume":"64","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6590-6220","authenticated-orcid":false,"given":"Sebastiaan J. C.","family":"Joosten","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0323-8829","authenticated-orcid":false,"given":"Ren\u00e9","family":"Thiemann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8872-2240","authenticated-orcid":false,"given":"Akihisa","family":"Yamada","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,12,9]]},"reference":[{"key":"9504_CR1","unstructured":"Avanzini, M., Sternagel, C., Thiemann, R.: Certification of complexity proofs using CeTA. In: RTA 2015. pp. 23\u201339. LIPIcs 36 (2015)"},{"issue":"3","key":"9504_CR2","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1145\/355791.355795","volume":"4","author":"WS Brown","year":"1978","unstructured":"Brown, W.S.: The subresultant PRS algorithm. ACM Trans. Math. Softw. 4(3), 237\u2013249 (1978)","journal-title":"ACM Trans. Math. Softw."},{"issue":"4","key":"9504_CR3","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1145\/321662.321665","volume":"18","author":"WS Brown","year":"1971","unstructured":"Brown, W.S., Traub, J.F.: On Euclid\u2019s algorithm and the theory of subresultants. J. ACM 18(4), 505\u2013514 (1971)","journal-title":"J. ACM"},{"key":"9504_CR4","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-642-32347-8_6","volume-title":"Interactive Theorem Proving","author":"Cyril Cohen","year":"2012","unstructured":"Cohen, C.: Construction of real algebraic numbers in Coq. In: ITP\u00a02012. LNCS, vol. 7406, pp. 67\u201382 (2012)"},{"key":"9504_CR5","doi-asserted-by":"crossref","unstructured":"Cohen, C., Djalal, B.: Formalization of a Newton series representation of polynomials. In: CPP\u00a02016. pp. 100\u2013109. ACM (2016)","DOI":"10.1145\/2854065.2854075"},{"issue":"1:02","key":"9504_CR6","first-page":"1","volume":"8","author":"C Cohen","year":"2012","unstructured":"Cohen, C., Mahboubi, A.: Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination. Log. Methods Comput. Sci. 8(1:02), 1\u201340 (2012)","journal-title":"Log. Methods Comput. Sci."},{"key":"9504_CR7","doi-asserted-by":"crossref","unstructured":"Divas\u00f3n, J., Joosten, S., Thiemann, R., Yamada, A.: A formalization of the Berlekamp-Zassenhaus factorization algorithm. In: CPP 2017, pp. 17\u201329 (2017)","DOI":"10.1145\/3018610.3018617"},{"key":"9504_CR8","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/S0022-4049(98)00081-4","volume":"145","author":"L Ducos","year":"2000","unstructured":"Ducos, L.: Optimizations of the subresultant algorithm. J. Pure Appl. Algebra 145, 149\u2013163 (2000)","journal-title":"J. Pure Appl. Algebra"},{"key":"9504_CR9","doi-asserted-by":"crossref","unstructured":"Eberl, M.: A decision procedure for univariate real polynomials in Isabelle\/HOL. In: CPP 2015. pp. 75\u201383. ACM (2015)","DOI":"10.1145\/2676724.2693166"},{"key":"9504_CR10","unstructured":"Eberl, M.: Linear recurrences. Archive of Formal Proofs (Oct 2017), \nhttp:\/\/isa-afp.org\/entries\/Linear_Recurrences.html\n\n, Formal proof development"},{"key":"9504_CR11","unstructured":"von\u00a0zur Gathen, J., Gerhard, J.: Modern computer algebra, 2nd edn. Cambridge University Press, Cambridge (2003)"},{"key":"9504_CR12","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-319-21401-6_6","volume-title":"Automated Deduction - CADE-25","author":"J\u00fcrgen Giesl","year":"2015","unstructured":"Giesl, J., Mesnard, F., Rubio, A., Thiemann, R., Waldmann, J.: Termination competition (termCOMP 2015). In: CADE 2015. LNCS, vol. 9195, pp. 105\u2013108 (2015)"},{"key":"9504_CR13","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1007\/978-3-642-39634-2_10","volume-title":"Interactive Theorem Proving","author":"Florian Haftmann","year":"2013","unstructured":"Haftmann, F., Krauss, A., Kun\u010dar, O., Nipkow, T.: Data refinement in Isabelle\/HOL. In: ITP\u00a02013. LNCS, vol. 7998, pp. 100\u2013115 (2013)"},{"key":"9504_CR14","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-319-03545-1_9","volume-title":"Certified Programs and Proofs","author":"Brian Huffman","year":"2013","unstructured":"Huffman, B., Kun\u010dar, O.: Lifting and transfer: a modular design for quotients in Isabelle\/HOL. In: CPP 2013. LNCS, vol. 8307, pp. 131\u2013146 (2013)"},{"issue":"2","key":"9504_CR15","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/0020-0190(82)90107-7","volume":"15","author":"JP Jouannaud","year":"1982","unstructured":"Jouannaud, J.P., Lescanne, P.: On multiset orderings. Inf. Process. Lett. 15(2), 57\u201363 (1982)","journal-title":"Inf. Process. Lett."},{"key":"9504_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.4204\/EPTCS.43.1","volume":"43","author":"Alexander Krauss","year":"2010","unstructured":"Krauss, A.: Recursive definitions of monadic functions. In: PAR 2010. EPTCS, vol.\u00a043, pp. 1\u201313 (2010)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"9504_CR17","unstructured":"Li, W.: Count the number of complex roots. Archive of Formal Proofs (Oct 2017), \nhttp:\/\/isa-afp.org\/entries\/Count_Complex_Roots.html\n\n, Formal proof development"},{"key":"9504_CR18","doi-asserted-by":"crossref","unstructured":"Li, W., Paulson, L.C.: A modular, efficient formalisation of real algebraic numbers. In: CPP\u00a02016. pp. 66\u201375. ACM (2016)","DOI":"10.1145\/2854065.2854074"},{"key":"9504_CR19","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1007\/11814771_37","volume-title":"Automated Reasoning","author":"Assia Mahboubi","year":"2006","unstructured":"Mahboubi, A.: Proving formally the implementation of an efficient gcd algorithm for polynomials. In: IJCAR 2006. LNCS, vol. 4130, pp. 438\u2013452 (2006)"},{"key":"9504_CR20","volume-title":"Algorithmic Algebra. Texts and Monographs in Computer Science","author":"B Mishra","year":"1993","unstructured":"Mishra, B.: Algorithmic Algebra. Texts and Monographs in Computer Science. Springer, New York (1993)"},{"key":"9504_CR21","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L., Wenzel, M.: Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"9504_CR22","doi-asserted-by":"crossref","unstructured":"Niven, I.: Irrational Numbers. No.\u00a011 in Carus Mathematical Monographs, Mathematical Association of America (1956)","DOI":"10.5948\/9781614440116"},{"key":"9504_CR23","doi-asserted-by":"crossref","unstructured":"Prasolov, V.V.: Polynomials. Springer (2004)","DOI":"10.1007\/978-3-642-03980-5"},{"key":"9504_CR24","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/978-3-319-43144-4_24","volume-title":"Interactive Theorem Proving","author":"Ren\u00e9 Thiemann","year":"2016","unstructured":"Thiemann, R., Yamada, A.: Algebraic numbers in Isabelle\/HOL. In: ITP 2016. LNCS, vol. 9807, pp. 391\u2013408 (2016)"},{"key":"9504_CR25","doi-asserted-by":"crossref","unstructured":"Thiemann, R., Yamada, A.: Formalizing Jordan normal forms in Isabelle\/HOL. In: CPP\u00a02016. pp. 88\u201399. ACM (2016)","DOI":"10.1145\/2854065.2854073"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-09504-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-018-09504-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-09504-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,2,29]],"date-time":"2020-02-29T04:03:02Z","timestamp":1582948982000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-018-09504-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,12,9]]},"references-count":25,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2020,3]]}},"alternative-id":["9504"],"URL":"https:\/\/doi.org\/10.1007\/s10817-018-09504-w","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2018,12,9]]},"assertion":[{"value":"10 October 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 November 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 December 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}