{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:12:21Z","timestamp":1775790741239,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":18,"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:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001665","name":"Agence Nationale de la Recherche","doi-asserted-by":"publisher","award":["ANR-18-CE25-0014"],"award-info":[{"award-number":["ANR-18-CE25-0014"]}],"id":[{"id":"10.13039\/501100001665","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.3575683","type":"proceedings-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T22:27:08Z","timestamp":1673476028000},"page":"167-181","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin\u2019s Data Types with Coq-Elpi"],"prefix":"10.1145","author":[{"given":"Benjamin","family":"Gr\u00e9goire","sequence":"first","affiliation":[{"name":"Universit\u00e9 C\u00f4te d\u2019Azur, France \/ Inria, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Christophe","family":"L\u00e9chenet","sequence":"additional","affiliation":[{"name":"Universit\u00e9 C\u00f4te d\u2019Azur, France \/ Inria, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Enrico","family":"Tassi","sequence":"additional","affiliation":[{"name":"Universit\u00e9 C\u00f4te d\u2019Azur, France \/ Inria, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133956.3134078"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40000.2020.00028"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3319535.3363211"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11916277_18"},{"key":"e_1_3_2_1_6_1","volume-title":"Bowman","author":"Chan Jonathan","year":"2019","unstructured":"Jonathan Chan and William J. Bowman. 2019. Practical Sized Typing for Coq. CoRR, abs\/1912.05601 (2019), arXiv:1912.05601. arxiv:1912.05601"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","unstructured":"Arthur Azevedo de Amorim. 2021. Deriving. https:\/\/doi.org\/10.5281\/zenodo.7065501 10.5281\/zenodo.7065501","DOI":"10.5281\/zenodo.7065501"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_32"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110278"},{"key":"e_1_3_2_1_10_1","unstructured":"Lucas Escot and Jesper Cockx. [n.d.]. generics library. https:\/\/github.com\/flupe\/generics"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16242-8_24"},{"key":"e_1_3_2_1_12_1","unstructured":"Jason Gross. [n.d.]. Scheme Equality is slow and generates enormous proof terms. https:\/\/github.com\/coq\/coq\/issues\/8517"},{"key":"e_1_3_2_1_13_1","unstructured":"Jason Gross and Andres Erbsen. 2022. 10 Years of Superlinear Slowness in Coq. https:\/\/jasongross.github.io\/papers\/2022-superlinear-slowness-coq-workshop.pdf Presented at"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/AAI28810898"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45231-5_18"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341690"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2019.29"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","unstructured":"The Coq Development Team. 2022. The Coq Proof Assistant. https:\/\/doi.org\/10.5281\/zenodo.5846982 10.5281\/zenodo.5846982","DOI":"10.5281\/zenodo.5846982"},{"key":"e_1_3_2_1_20_1","unstructured":"The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. https:\/\/homotopytypetheory.org\/book Institute for Advanced Study."}],"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.3575683","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3573105.3575683","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.3575683"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,11]]},"references-count":18,"alternative-id":["10.1145\/3573105.3575683","10.1145\/3573105"],"URL":"https:\/\/doi.org\/10.1145\/3573105.3575683","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"}}]}}