{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,28]],"date-time":"2026-01-28T04:17:27Z","timestamp":1769573847008,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":23,"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\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100003246","name":"Nederlandse Organisatie voor Wetenschappelijk Onderzoek","doi-asserted-by":"publisher","award":["016.Vidi.189.037"],"award-info":[{"award-number":["016.Vidi.189.037"]}],"id":[{"id":"10.13039\/501100003246","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,1,11]]},"DOI":"10.1145\/3573105.3575671","type":"proceedings-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T22:27:08Z","timestamp":1673476028000},"page":"253-266","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":16,"title":["Aesop: White-Box Best-First Proof Search for Lean"],"prefix":"10.1145","author":[{"given":"Jannis","family":"Limperg","sequence":"first","affiliation":[{"name":"Vrije Universiteit Amsterdam, Netherlands"}]},{"given":"Asta Halkj\u00e6r","family":"From","sequence":"additional","affiliation":[{"name":"DTU, Denmark"}]}],"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-642-22438-6_7"},{"key":"e_1_3_2_1_2_1","volume-title":"ICML","author":"Bansal Kshitij","year":"2019","unstructured":"Kshitij Bansal, Sarah Loos, Markus Rabe, Christian Szegedy, and Stewart Wilcox. 2019. HOList: an environment for machine learning of higher order logic theorem proving. In ICML 2019. 454\u2013463. https:\/\/proceedings.mlr.press\/v97\/bansal19a.html"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.6092\/issn.1972-5787"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373824"},{"key":"e_1_3_2_1_5_1","volume-title":"Workshop on Industrial-Strength Formal Specification Techniques","author":"Crow Judy","year":"1995","unstructured":"Judy Crow, Sam Owre, John Rushby, Natarajan Shankar, and Mandayam Srivas. 1995. A Tutorial Introduction to PVS. In Workshop on Industrial-Strength Formal Specification Techniques 1995. http:\/\/www.csl.sri.com\/papers\/wift-tutorial\/"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51054-1_3"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-020-09580-x"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45744-5_46"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","unstructured":"Jesse Michael Han Jason Rute Yuhuai Wu Edward W. Ayers and Stanislas Polu. 2021. Proof artifact co-training for theorem proving with language models. https:\/\/doi.org\/10.48550\/ARXIV.2102.06203","DOI":"10.48550\/ARXIV.2102.06203"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/CMPASS.1996.507872"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10958-005-0090-6"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","unstructured":"Guillaume Lample Marie-Anne Lachaux Thibaut Lavril Xavier Martinet Amaury Hayat Gabriel Ebner Aur\u00e9lien Rodriguez and Timoth\u00e9e Lacroix. 2022. HyperTree proof search for neural theorem proving. https:\/\/doi.org\/10.48550\/ARXIV.2205.11491","DOI":"10.48550\/ARXIV.2205.11491"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/11617990_10"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00245458"},{"key":"e_1_3_2_1_17_1","volume-title":"Towards a practical programming language based on dependent type theory. Ph. D. Dissertation","author":"Norell Ulf","unstructured":"Ulf Norell. 2007. Towards a practical programming language based on dependent type theory. Ph. D. Dissertation. Chalmers University of Technology. G\u00f6teborg, Sweden. https:\/\/www.cse.chalmers.se\/~ulfn\/papers\/thesis.pdf"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.48456\/tr-396"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.3217\/jucs-005-03-0073"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-019-00492-1"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9407-7"},{"key":"e_1_3_2_1_22_1","volume-title":"PAAR","author":"Villadsen J\u00f8rgen","year":"2020","unstructured":"J\u00f8rgen Villadsen. 2020. A micro prover for teaching automated reasoning. In PAAR 2020."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-43144-4_27"}],"event":{"name":"CPP '23: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs","location":"Boston MA USA","acronym":"CPP '23","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"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.3575671","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3573105.3575671","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:45:37Z","timestamp":1750178737000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3573105.3575671"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,11]]},"references-count":23,"alternative-id":["10.1145\/3573105.3575671","10.1145\/3573105"],"URL":"https:\/\/doi.org\/10.1145\/3573105.3575671","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"}}]}}