{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:09:01Z","timestamp":1762459741436,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":12,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,7,8]],"date-time":"2019-07-08T00:00:00Z","timestamp":1562544000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Deutsche Forschungsgemeinschaft","award":["NI 491\/16-1"],"award-info":[{"award-number":["NI 491\/16-1"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,7,8]]},"DOI":"10.1145\/3326229.3326240","type":"proceedings-article","created":{"date-parts":[[2019,7,9]],"date-time":"2019-07-09T12:53:20Z","timestamp":1562676800000},"page":"147-154","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Verified Real Asymptotics in Isabelle\/HOL"],"prefix":"10.1145","author":[{"given":"Manuel","family":"Eberl","sequence":"first","affiliation":[{"name":"Technical University Munich, Munich, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,7,8]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Julian Biendarra Jasmin Christian Blanchette Aymeric Bouzy Martin Desharnais Mathias Fleury Johannes H\u00f6lzl Ondvr ej Kunvc ar Andreas Lochbihler Fabian Meier Lorenz Panny Andrei Popescu Christian Sternagel Ren\u00e9 Thiemann and Dmitriy Traytel. 2017. Foundational (Co)datatypes and (Co)recursion for Higher-Order Logic. In Frontiers of Combining Systems Clare Dixon and Marcelo Finger (Eds.). Springer International Publishing Cham 3--21.","key":"e_1_3_2_1_1_1","DOI":"10.1007\/978-3-319-66167-4_1"},{"unstructured":"Nicolas Bourbaki. 1971. Topologie g\u00e9n\u00e9rale.","key":"e_1_3_2_1_2_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_3_1","DOI":"10.1007\/s10817-016-9378-0"},{"key":"e_1_3_2_1_5_1","volume-title":"Proceedings of the ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS'09)","author":"H\u00f6lzl Johannes","year":"2009","unstructured":"Johannes H\u00f6lzl. 2009. Proving Inequalities over Reals with Computation in Isabelle\/HOL. In Proceedings of the ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS'09),, Gabriel Dos Reis and Laurent Th\u00e9ry (Eds.). Munich, 38--45."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_6_1","DOI":"10.1007\/978-3-642-39634-2_21"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_7_1","DOI":"10.1145\/220346.220360"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_8_1","DOI":"10.1145\/236869.237089"},{"unstructured":"Udo Richter. 2005. Automatische Berechnung von Grenzwerten und Implementierung in Mathematica. diploma thesis. Universit\u00e4t Kassel.","key":"e_1_3_2_1_9_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_10_1","DOI":"10.1112\/jlms\/jdq057"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_11_1","DOI":"10.1016\/S0747-7171(08)80161-7"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_12_1","DOI":"10.5555\/993959"},{"key":"e_1_3_2_1_14_1","series-title":"Lecture Notes in Mathematics","volume-title":"Transseries and real differential algebra","author":"van der Hoeven Joris","unstructured":"Joris van der Hoeven. 2006. Transseries and real differential algebra. Lecture Notes in Mathematics, Vol. 1888. Springer-Verlag."}],"event":{"sponsor":["SIGSAM ACM Special Interest Group on Symbolic and Algebraic Manipulation"],"acronym":"ISSAC '19","name":"ISSAC '19: International Symposium on Symbolic and Algebraic Computation","location":"Beijing China"},"container-title":["Proceedings of the 2019 International Symposium on Symbolic and Algebraic Computation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3326229.3326240","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3326229.3326240","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:25:59Z","timestamp":1750206359000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3326229.3326240"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,8]]},"references-count":12,"alternative-id":["10.1145\/3326229.3326240","10.1145\/3326229"],"URL":"https:\/\/doi.org\/10.1145\/3326229.3326240","relation":{},"subject":[],"published":{"date-parts":[[2019,7,8]]},"assertion":[{"value":"2019-07-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}