{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:10:07Z","timestamp":1750219807070,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":30,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T00:00:00Z","timestamp":1673395200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-sa\/4.0\/"}],"funder":[{"name":"NWO","award":["016.Vidi.189.037, 639.032.613"],"award-info":[{"award-number":["016.Vidi.189.037, 639.032.613"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,1,11]]},"DOI":"10.1145\/3573105.3575682","type":"proceedings-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T22:27:08Z","timestamp":1673476028000},"page":"47-62","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Formalized Class Group Computations and Integral Points on Mordell Elliptic Curves"],"prefix":"10.1145","author":[{"given":"Anne","family":"Baanen","sequence":"first","affiliation":[{"name":"Vrije Universiteit Amsterdam, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alex J.","family":"Best","sequence":"additional","affiliation":[{"name":"Vrije Universiteit Amsterdam, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nirvana","family":"Coppola","sequence":"additional","affiliation":[{"name":"Vrije Universiteit Amsterdam, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sander R.","family":"Dahmen","sequence":"additional","affiliation":[{"name":"Vrije Universiteit Amsterdam, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51054-1_1"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2022.4"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2021.5"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Alan Baker. 1968. Contributions to the Theory of Diophantine Equations. II. the Diophantine Equation y^2 = x^3 + k. Philosophical Transactions of the Royal Society of London. Series A Mathematical and Physical Sciences 263 1139 (1968) 193\u2013208. issn:00804614 http:\/\/www.jstor.org\/stable\/73429","DOI":"10.1098\/rsta.1968.0011"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1112\/S1461157015000182"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-49923-9"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2022.14"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79876-5_37"},{"volume-title":"Diophantus","author":"Delahaye David","key":"e_1_3_2_1_10_1","unstructured":"David Delahaye and Micaela Mayero. 2005. Diophantus\u2019 20th Problem and Fermat\u2019s Last Theorem for n=4: Formalization of Fermat\u2019s Proofs in the Coq Proof Assistant. Draft. arxiv:cs\/0510011"},{"key":"e_1_3_2_1_11_1","unstructured":"Leonard E. Dickson. 1920. History of the theory of numbers. 2 Carnegie Institution of Washington."},{"key":"e_1_3_2_1_12_1","volume-title":"Foote","author":"Dummit David S.","year":"2004","unstructured":"David S. Dummit and Richard M. Foote. 2004. Abstract algebra (third ed.). John Wiley & Sons, Inc., Hoboken, NJ. isbn:0-471-43334-9"},{"key":"e_1_3_2_1_13_1","unstructured":"Manuel Eberl. 2017. Minkowski\u2019s Theorem. Archive of Formal Proofs July issn:2150-914x https:\/\/isa-afp.org\/entries\/Minkowskis_Theorem.html"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-9307-8"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_7"},{"key":"e_1_3_2_1_16_1","unstructured":"S. Lang. 2005. Undergraduate Algebra. Springer New York. isbn:9780387220253 lccn:2004049194"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2019.27"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.262.4"},{"key":"e_1_3_2_1_19_1","volume-title":"Lewis and Paul-Nicolas Madelaine","author":"Robert","year":"2020","unstructured":"Robert Y. Lewis and Paul-Nicolas Madelaine. 2020. Simplifying Casts and Coercions (Extended Abstract). In Practical Aspects of Automated Reasoning, Pascal Fontaine, Konstantin Korovin, Ilias S. Kotsireas, Philipp R\u00fcmmer, and Sophie Tourret (Eds.) (CEUR Workshop Proceedings, Vol. 2752). CEUR-WS.org, Aachen, Germany. 53\u201362. http:\/\/ceur-ws.org\/Vol-2752\/paper4.pdf"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-021-09611-1"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s2-13.1.60"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s2-18.1.1-s"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1112\/plms\/s2-21.1.415"},{"volume-title":"Diophantine equations","author":"Mordell Louis","key":"e_1_3_2_1_24_1","unstructured":"Louis Mordell. 1969. Diophantine equations. Academic Press. isbn:9780080873428"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03983-0"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2022.26"},{"key":"e_1_3_2_1_28_1","volume-title":"Tabled Typeclass Resolution. CoRR, abs\/2001.04301","author":"Selsam Daniel","year":"2020","unstructured":"Daniel Selsam, Sebastian Ullrich, and Leonardo de Moura. 2020. Tabled Typeclass Resolution. CoRR, abs\/2001.04301 (2020), arXiv:2001.04301. arxiv:2001.04301"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.4064\/aa-24-3-251-259"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373824"},{"key":"e_1_3_2_1_31_1","unstructured":"The Sage Developers. 2022. SageMath the Sage Mathematics Software System (Version 9.7). https:\/\/www.sagemath.org"}],"event":{"name":"CPP '23: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Boston MA USA","acronym":"CPP '23"},"container-title":["Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3573105.3575682","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3573105.3575682","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:45:38Z","timestamp":1750178738000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3573105.3575682"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,11]]},"references-count":30,"alternative-id":["10.1145\/3573105.3575682","10.1145\/3573105"],"URL":"https:\/\/doi.org\/10.1145\/3573105.3575682","relation":{},"subject":[],"published":{"date-parts":[[2023,1,11]]},"assertion":[{"value":"2023-01-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}