{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:05:23Z","timestamp":1750309523122,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":45,"publisher":"ACM","license":[{"start":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T00:00:00Z","timestamp":1736467200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-sa\/4.0\/"}],"funder":[{"name":"Nederlandse Organisatie voor Wetenschappelijk Onderzoek","award":["613.009.143, Formalizing Diophantine algorithms"],"award-info":[{"award-number":["613.009.143, Formalizing Diophantine algorithms"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,1,10]]},"DOI":"10.1145\/3703595.3705874","type":"proceedings-article","created":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T21:23:16Z","timestamp":1736544196000},"page":"50-66","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Certifying Rings of Integers in Number Fields"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8497-3683","authenticated-orcid":false,"given":"Anne","family":"Baanen","sequence":"first","affiliation":[{"name":"Vrije Universiteit Amsterdam, Amsterdam, Netherlands"},{"name":"Lean FRO, Cambridge, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-5203-4781","authenticated-orcid":false,"given":"Alain","family":"Chavarri Villarello","sequence":"additional","affiliation":[{"name":"Vrije Universiteit Amsterdam, Amsterdam, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0014-0789","authenticated-orcid":false,"given":"Sander R.","family":"Dahmen","sequence":"additional","affiliation":[{"name":"Vrije Universiteit Amsterdam, Amsterdam, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,1,10]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-52200-1_46"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-016-0383-1"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9379-z"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51054-1_2"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3573105.3575682"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-022-09644-0"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.1996.0125"},{"key":"e_1_3_2_2_8_1","unstructured":"Viktor Bouniakowsky. 1854. Sur les diviseurs num\u00e9riques invariables des fonctions rationnelles entieres. De l\u2019Imprimerie de l\u2019Acad\u00e9mie imp\u00e9riale des sciences."},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_7"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.2307\/2006403"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1080\/10586458.2021.1986176"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.5802\/jtnb.113"},{"key":"e_1_3_2_2_13_1","unstructured":"Mario Carneiro. 2019. The Type Theory of Lean. https:\/\/github.com\/digama0\/lean-type-theory\/releases MSc thesis"},{"key":"e_1_3_2_2_14_1","unstructured":"Augustin Louis Baron Cauchy. 1829. Exercices de math\u00e9matiques (\u0152 uvres 2 Vol. 9)."},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","unstructured":"Alain Chavarri Villarello Sander Dahmen and Anne Baanen. 2024. Certifying rings of integers in number fields. https:\/\/doi.org\/10.5281\/zenodo.14283856 10.5281\/zenodo.14283856","DOI":"10.5281\/zenodo.14283856"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57262-3_10"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-02945-9"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3437992.3439919"},{"key":"e_1_3_2_2_19_1","first-page":"3","article-title":"Ueber den Zusammenhang zwischen der Theorie der ideale und der Theorie der h\u00f6heren Congruenzen","volume":"23","author":"Dedekind R.","year":"1878","unstructured":"R. Dedekind. 1878. Ueber den Zusammenhang zwischen der Theorie der ideale und der Theorie der h\u00f6heren Congruenzen. Abhandlungen der K\u00f6niglichen Gesellschaft der Wissenschaften in G\u00f6ttingen, 23 (1878), 3\u201338. http:\/\/eudml.org\/doc\/135827","journal-title":"Abhandlungen der K\u00f6niglichen Gesellschaft der Wissenschaften in G\u00f6ttingen"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32347-8_7"},{"key":"e_1_3_2_2_21_1","volume-title":"Foote","author":"Dummit David S.","year":"2004","unstructured":"David S. Dummit and Richard M. Foote. 2004. Abstract algebra (third edition ed.). John Wiley & Sons, Inc., Hoboken, NJ, USA. isbn:0-471-43334-9"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.4230\/lipics.itp.2022.10"},{"key":"e_1_3_2_2_23_1","unstructured":"Manuel Eberl. 2020. Gaussian Integers. Archive of Formal Proofs April issn:2150-914x https:\/\/isa-afp.org\/entries\/Gaussian_Integers.html"},{"key":"e_1_3_2_2_24_1","volume-title":"ON THE COMPUTATION OF THE MAXIMAL ORDER IN A DEDEKIND DOMAIN. ProQuest LLC","author":"Ford David James","year":"2004","unstructured":"David James Ford. 1978. ON THE COMPUTATION OF THE MAXIMAL ORDER IN A DEDEKIND DOMAIN. ProQuest LLC, Ann Arbor, MI. http:\/\/gateway.proquest.com\/openurl?url_ver=Z39.88-2004&rft_val_fmt=info:ofi\/fmt:kev:mtx:dissertation&res_dat=xri:pqdiss&rft_dat=xri:pqdiss:7902127 Thesis (Ph.D.)\u2013The Ohio State University"},{"key":"e_1_3_2_2_25_1","first-page":"2521","volume-title":"2012 International Symposium on Information Theory and its Applications. 591\u2013595","author":"Futa Yuichi","year":"2012","unstructured":"Yuichi Futa, Daichi Mizushima, and Hiroyuki Okazaki. 2012. Formalization of Gaussian integers, Gaussian rational numbers, and their algebraic structures with Mizar. In 2012 International Symposium on Information Theory and its Applications. 591\u2013595. isbn:978-1-4673-2521-9"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_7"},{"key":"e_1_3_2_2_27_1","unstructured":"Markus Himmel. 2024. Formalization of Pratt Certificates. https:\/\/github.com\/leanprover-community\/mathlib4\/blob\/6439ce3f194a2acd309af6831d753e560c46bcf6\/Mathlib\/NumberTheory\/LucasPrimality.lean Accessed: 2024-09-06"},{"volume-title":"Handbook of linear algebra","key":"e_1_3_2_2_28_1","unstructured":"2014. Handbook of linear algebra (second ed.), Leslie Hogben (Ed.). CRC Press, Boca Raton, FL. isbn:978-1-4665-0728-9"},{"key":"e_1_3_2_2_29_1","unstructured":"Joseph-Louis Lagrange. 1798. Trait\u00e9 de la r\u00e9solution des \u00e9quations num\u00e9riques Paris (1798). \u0152 uvres de Lagrange. 8 (1798) 637\u2013649."},{"volume-title":"Algebra","author":"Lang Serge","key":"e_1_3_2_2_30_1","unstructured":"Serge Lang. 2002. Algebra (third edition ed.) (Graduate Texts in Mathematics, Vol. 211). Springer. isbn:0-387-95385-X"},{"key":"e_1_3_2_2_31_1","unstructured":"Serge Lang. 2005. Undergraduate Algebra. Springer. isbn:9780387220253 lccn:2004049194"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.262.4"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-021-09611-1"},{"key":"e_1_3_2_2_34_1","volume-title":"The L-functions and modular forms database. https:\/\/www.lmfdb.org [Online","author":"Collaboration The LMFDB","year":"2024","unstructured":"The LMFDB Collaboration. 2024. The L-functions and modular forms database. https:\/\/www.lmfdb.org [Online; accessed 17 September 2024]"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-17(1:16)2021"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","unstructured":"Assia Mahboubi and Enrico Tassi. 2020. Mathematical Components. Zenodo. https:\/\/doi.org\/10.5281\/zenodo.4282710 10.5281\/zenodo.4282710","DOI":"10.5281\/zenodo.4282710"},{"key":"e_1_3_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03983-0"},{"key":"e_1_3_2_2_38_1","unstructured":"M. Pohst and H. Zassenhaus. 1997. Algorithmic algebraic number theory (Encyclopedia of Mathematics and its Applications Vol. 30). Cambridge University Press Cambridge. isbn:0-521-59669-6 Revised reprint of the 1989 original"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1137\/0209024"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF03027290"},{"key":"e_1_3_2_2_41_1","unstructured":"2023. PARI\/GP version 2.15.4. available from http:\/\/pari.math.u-bordeaux.fr\/"},{"key":"e_1_3_2_2_42_1","unstructured":"The Sage Developers. 2024. SageMath the Sage Mathematics Software System (Version 10.3). https:\/\/www.sagemath.org"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-020-09552-1"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139856065"},{"key":"e_1_3_2_2_45_1","volume-title":"Scalar actions in Lean\u2019s mathlib. CoRR, abs\/2108.10700","author":"Wieser Eric","year":"2021","unstructured":"Eric Wieser. 2021. Scalar actions in Lean\u2019s mathlib. CoRR, abs\/2108.10700 (2021), arXiv:2108.10700."}],"event":{"name":"CPP '25: 14th ACM SIGPLAN International Conference on Certified Programs and Proofs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG"],"location":"Denver CO USA","acronym":"CPP '25"},"container-title":["Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3703595.3705874","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3703595.3705874","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:18:08Z","timestamp":1750295888000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3703595.3705874"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,10]]},"references-count":45,"alternative-id":["10.1145\/3703595.3705874","10.1145\/3703595"],"URL":"https:\/\/doi.org\/10.1145\/3703595.3705874","relation":{},"subject":[],"published":{"date-parts":[[2025,1,10]]},"assertion":[{"value":"2025-01-10","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}