{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:57:08Z","timestamp":1776333428135,"version":"3.51.2"},"publisher-location":"New York, NY, USA","reference-count":35,"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"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,1,11]]},"DOI":"10.1145\/3573105.3575676","type":"proceedings-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T22:27:08Z","timestamp":1673476028000},"page":"63-77","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Compositional Pre-processing for Automated Reasoning in Dependent Type Theory"],"prefix":"10.1145","author":[{"given":"Valentin","family":"Blot","sequence":"first","affiliation":[{"name":"LMF, France \/ Inria, France \/ University of Paris-Saclay, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Denis","family":"Cousineau","sequence":"additional","affiliation":[{"name":"Mitsubishi, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Enzo","family":"Crance","sequence":"additional","affiliation":[{"name":"Nantes Universit\u00e9, France \/ \u00c9cole Centrale Nantes, France \/ CNRS, France \/ Inria, France \/ LS2N, France \/ UMR 6004, France \/ Mitsubishi, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Louise Dubois","family":"de Prisque","sequence":"additional","affiliation":[{"name":"LMF, France \/ Inria, France \/ University of Paris-Saclay, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chantal","family":"Keller","sequence":"additional","affiliation":[{"name":"LMF, France \/ University of Paris-Saclay, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Assia","family":"Mahboubi","sequence":"additional","affiliation":[{"name":"Nantes Universit\u00e9, France \/ \u00c9cole Centrale Nantes, France \/ CNRS, France \/ Inria, France \/ LS2N, France \/ UMR 6004, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Pierre","family":"Vial","sequence":"additional","affiliation":[{"name":"Inria, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Lennart Beringer and Josiah Dodds","author":"Appel Qinxiang Cao","year":"2022","unstructured":"Qinxiang Cao Andrew W. Appel, Lennart Beringer and Josiah Dodds. 2022. Verifiable C. https:\/\/github.com\/PrincetonUniversity\/VST\/raw\/master\/doc\/VC.pdf"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19718-5_1"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29436-6_3"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74464-1_4"},{"key":"e_1_3_2_1_5_1","volume-title":"Coq Workshop on Programming Languages.  https:\/\/popl17","author":"Besson Fr\u00e9d\u00e9ric","year":"2017","unstructured":"Fr\u00e9d\u00e9ric Besson. 2017. ppsimpl: a reflexive Coq tactic for canonising goals. In Coq Workshop on Programming Languages. https:\/\/popl17.sigplan.org\/details\/main\/3\/ppsimpl-a-reflexive-Coq-tactic-for-canonising-goals"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2021.9"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.336.3"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-24364-6_7"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_12"},{"key":"e_1_3_2_1_10_1","volume-title":"Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant","author":"Chlipala Adam","unstructured":"Adam Chlipala. 2013. Certified Programming with Dependent Types - A Pragmatic Introduction to the Coq Proof Assistant. MIT Press. isbn:978-0-262-02665-9 http:\/\/mitpress.mit.edu\/books\/certified-programming-dependent-types"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.TYPES.2016.9"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9458-4"},{"key":"e_1_3_2_1_13_1","volume-title":"Trakt: a generic pre-processing tactic for theory-based proof automation. Abstract and talk at the Coq Workshop","author":"Denis Cousineau Enzo Crance","year":"2022","unstructured":"Enzo Crance Denis Cousineau and Assia Mahboubi. 2022. Trakt: a generic pre-processing tactic for theory-based proof automation. Abstract and talk at the Coq Workshop 2022, https:\/\/www.youtube.com\/watch?v=dZyylCY1seE"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2022.8"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_7"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_7"},{"key":"e_1_3_2_1_17_1","volume-title":"Langages Applicatifs (Annual Workshop). INRIA.","author":"Ledein Am\u00e9lie","year":"2020","unstructured":"Am\u00e9lie Ledein and Catherine Dubois. 2020. FaCiLe en Coq : v\u00e9rification formelle des listes d\u2019intervalles. In JFLA\u201920 : Journ\u00e9es Francophones sur les Langages Applicatifs (Annual Workshop). INRIA."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9099-0"},{"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 Joint Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 5th Satisfiability Checking and Symbolic Computation Workshop (SC-Square) Workshop, 2020 co-located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020), Paris, France, June-July, 2020 (Virtual), Pascal Fontaine, Konstantin Korovin, Ilias S. Kotsireas, Philipp R\u00fcmmer, and Sophie Tourret (Eds.) (CEUR Workshop Proceedings, Vol. 2752). CEUR-WS.org, 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\/978-3-642-39634-2_5"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","unstructured":"Assia Mahboubi and Enrico Tassi. 2021. Mathematical Components. Zenodo. https:\/\/doi.org\/10.5281\/zenodo.4457887 10.5281\/zenodo.4457887","DOI":"10.5281\/zenodo.4457887"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_2"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/11617990_12"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_22"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44957-4_16"},{"key":"e_1_3_2_1_26_1","volume-title":"Chris Casinghino, Marco Gaboardi, Michael Greenberg, C\u01cet\u01celin Hri\u0163cu, Vilhelm Sj\u00f6berg, and Brent Yorgey.","author":"Pierce Benjamin C.","year":"2018","unstructured":"Benjamin C. Pierce, Arthur Azevedo de Amorim, Chris Casinghino, Marco Gaboardi, Michael Greenberg, C\u01cet\u01celin Hri\u0163cu, Vilhelm Sj\u00f6berg, and Brent Yorgey. 2018. Logical Foundations. Electronic textbook. Version 5.5. http:\/\/www.cis.upenn.edu\/ bcpierce\/sf"},{"key":"e_1_3_2_1_27_1","unstructured":"Kazuhiko Sakaguchi. 2012-2020. A Formalization of Typed and Untyped \u03bb -Calculi in Coq and Agda2. https:\/\/github.com\/pi8027\/lambda-calculus"},{"key":"e_1_3_2_1_28_1","unstructured":"Kazuhiko Sakaguchi. 2019-2022. Micromega tactics for Mathematical Components. https:\/\/github.com\/math-comp\/mczify"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2022.29"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09540-0"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3429979"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ITP.2019.29"},{"key":"e_1_3_2_1_35_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"}],"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.3575676","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3573105.3575676","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.3575676"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,11]]},"references-count":35,"alternative-id":["10.1145\/3573105.3575676","10.1145\/3573105"],"URL":"https:\/\/doi.org\/10.1145\/3573105.3575676","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"}}]}}