{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T05:57:24Z","timestamp":1777874244950,"version":"3.51.4"},"publisher-location":"Cham","reference-count":86,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227195","type":"print"},{"value":"9783032227201","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T00:00:00Z","timestamp":1775779200000},"content-version":"vor","delay-in-days":99,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Dependently typed proof assistants offer powerful meta-programming features, which allow users to implement proof automation or compile-time code generation. This paper surveys meta-programming frameworks in Rocq, Agda, and Lean, with seven implementations of a running example: deriving instances for the  typeclass. This example is fairly simple, but realistic enough to highlight recurring difficulties with meta-programming: conceptual limitations of frameworks such as term representation \u2013 and in particular binder representation \u2013, meta-language expressiveness, and verifiability, as well as current limitations such as API completeness, learning curve, and prover state management, which could in principle be remedied. We conclude with insights regarding features an ideal meta-programming framework should provide.<\/jats:p>","DOI":"10.1007\/978-3-032-22720-1_7","type":"book-chapter","created":{"date-parts":[[2026,4,9]],"date-time":"2026-04-09T15:28:50Z","timestamp":1775748530000},"page":"166-189","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Code Generation via Meta-programming in Dependently Typed Proof Assistants"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-7817-9551","authenticated-orcid":false,"given":"Mathis","family":"Bouverot-Dupuis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8676-9819","authenticated-orcid":false,"given":"Yannick","family":"Forster","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,4,10]]},"reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Andreas Abel, Guillaume Allais, Aliya Hameer, Brigitte Pientka, Alberto Momigliano, Steven Sch\u00e4fer, and Kathrin Stark. POPLMark Reloaded: Mechanizing proofs by logical relations. J. Funct. Program., 29, 2019.","DOI":"10.1017\/S0956796819000170"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Danel Ahman, C\u0103t\u0103lin Hri\u0163cu, Kenji Maillard, Guido Mart\u00ednez, Gordon Plotkin, Jonathan Protzenko, Aseem Rastogi, and Nikhil Swamy. Dijkstra monads for free. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL \u201917, page 515\u2013529, New York, NY, USA, 2017. Association for Computing Machinery.","DOI":"10.1145\/3009837.3009878"},{"key":"7_CR3","unstructured":"Guillaume Allais and Andr\u00e9 Videla. Deriving for functor instances in idris 2 (idris 2 standard library)."},{"key":"7_CR4","unstructured":"Abhishek Anand, Andrew\u00a0W. Appel, Greg Morrisett, Zoe Paraskevopoulou, Randy Pollack, Olivier\u00a0Savary B\u00e9langer, Matthieu Sozeau, and Matthew\u00a0Z. Weaver. Certicoq : A verified compiler for coq. 2016."},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Abhishek Anand, Simon Boulier, Cyril Cohen, Matthieu Sozeau, and Nicolas Tabareau. Towards certified meta-programming with typed template-coq. In ITP 2018, pages 20\u201339, 2018.","DOI":"10.1007\/978-3-319-94821-8_2"},{"key":"7_CR6","unstructured":"Abhishek Anand, Anvay Grover, John Li, Greg Morrisett, Randy Pollack, Olivier\u00a0Savary Belanger, Matthew Weaver, Andrew Appel, Yannick Forster, Joomy Korkut, Zoe Paraskevopoulou, Kathrin Stark, and Matthieu Sozeau. Certicoq: A verified compiler for coq (github repository). accessed Feb 18th 2025, 2025."},{"key":"7_CR7","doi-asserted-by":"crossref","unstructured":"Danil Annenkov, Jakob\u00a0Botsch Nielsen, and Bas Spitters. Concert: a smart contract certification framework in coq. In Jasmin Blanchette and Catalin Hritcu, editors, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pages 215\u2013228. ACM, 2020.","DOI":"10.1145\/3372885.3373829"},{"key":"7_CR8","unstructured":"Ali Assaf, Guillaume Burel, Rapha\u00ebl Cauderlier, David Delahaye, Gilles Dowek, Catherine Dubois, Fr\u00e9d\u00e9ric Gilbert, Pierre Halmagrand, Olivier Hermant, and Ronan Saillard. Dedukti: a logical framework based on the $${\\lambda } \\Pi $$-calculus modulo theory. CoRR, abs\/2311.07185, 2023."},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Brian\u00a0E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J.\u00a0Nathan Foster, Benjamin\u00a0C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. Mechanized metatheory for the masses: The POPLMark challenge. In Joe Hurd and Tom Melham, editors, Theorem Proving in Higher Order Logics, pages 50\u201365, Berlin & Heidelberg, 2005. Springer.","DOI":"10.1007\/11541868_4"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Anne Baanen. A lean tactic for normalising ring expressions with exponents (short paper). In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning, pages 21\u201327, Cham, 2020. Springer International Publishing.","DOI":"10.1007\/978-3-030-51054-1_2"},{"key":"7_CR11","unstructured":"Andrej Bauer, Ga\u00ebtan Gilbert, Philipp\u00a0G. Haselwarter, Matija Pretnar, and Christopher\u00a0A. Stone. Design and Implementation of the Andromeda Proof Assistant. In Silvia Ghilezan, Herman Geuvers, and Jelena Ivetic, editors, 22nd International Conference on Types for Proofs and Programs (TYPES 2016), volume\u00a097 of Leibniz International Proceedings in Informatics (LIPIcs), pages 5:1\u20135:31, Dagstuhl, Germany, 2018. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik."},{"key":"7_CR12","doi-asserted-by":"crossref","unstructured":"Mathis Bouverot-Dupuis and Yannick Forster. Code Generation via Meta-programming in Dependently Typed Proof Assistants (extended version). working paper or preprint, January 2026.","DOI":"10.1007\/978-3-032-22720-1_7"},{"key":"7_CR13","doi-asserted-by":"crossref","unstructured":"Edwin\u00a0C. Brady. Idris, a general-purpose dependently typed programming language: Design and implementation. J. Funct. Program., 23(5):552\u2013593, 2013.","DOI":"10.1017\/S095679681300018X"},{"key":"7_CR14","unstructured":"Edwin\u00a0C. Brady. Idris 2: Quantitative type theory in practice. In Anders M\u00f8ller and Manu Sridharan, editors, 35th European Conference on Object-Oriented Programming, ECOOP 2021, July 11-17, 2021, Aarhus, Denmark (Virtual Conference), volume 194 of LIPIcs, pages 9:1\u20139:26. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2021."},{"key":"7_CR15","unstructured":"Mario Carneiro. Lean4lean: Towards a verified typechecker for lean, in lean, 2024."},{"key":"7_CR16","unstructured":"Tej Chajed. Record updates in coq. In CoqPL 2021: The Seventh International Workshop on Coq for Programming Languages, 2021. Extended Abstract."},{"key":"7_CR17","doi-asserted-by":"crossref","unstructured":"Adam Chlipala. Parametric higher-order abstract syntax for mechanized semantics. SIGPLAN Not., 43(9):143\u2013156, September 2008.","DOI":"10.1145\/1411203.1411226"},{"key":"7_CR18","unstructured":"Cyril Cohen, Enzo Crance, and Assia Mahboubi. Trocq: Proof transfer for free, with or without univalence. CoRR, abs\/2310.14022, 2023."},{"key":"7_CR19","unstructured":"Cyril Cohen, Kazuhiko Sakaguchi, and Enrico Tassi. Hierarchy builder: Algebraic hierarchies made easy in coq with elpi (system description). In Zena\u00a0M. Ariola, editor, 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference), volume 167 of LIPIcs, pages 34:1\u201334:21. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2020."},{"key":"7_CR20","unstructured":"Agda Community. agda-stdlib-classes."},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"Thierry Coquand and G\u00e9rard\u00a0P Huet. The calculus of constructions. Information and Computation, 76(2\/3):95\u2013120, 1988.","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"7_CR22","unstructured":"Enzo Crance. M\u00e9ta-programmation pour le transfert de preuve en th\u00e9orie des types d\u00e9pendants. Theses, Nantes Universit\u00e9, December 2023."},{"key":"7_CR23","unstructured":"Adrian Dapprich. Autosubst metacoq, 2021."},{"key":"7_CR24","unstructured":"Adrian Dapprich. Generating infrastructural code for terms with binders using metacoq, 2021. Bachelor\u2019s thesis, Saarland University."},{"key":"7_CR25","unstructured":"Arthur\u00a0Azevedo de\u00a0Amorim. Deriving instances with dependent types. In Proceedings of the Sixth International Workshop on Coq for Programming Languages (CoqPL 2020), 2020."},{"key":"7_CR26","doi-asserted-by":"crossref","unstructured":"N.G de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. Indagationes Mathematicae (Proceedings), 75(5):381\u2013392, 1972.","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"7_CR27","unstructured":"Louise\u00a0Dubois de\u00a0Prisque. Pr\u00e9traitement compositionnel en Coq. (Compositional preprocessing in Coq). PhD thesis, University of Paris-Saclay, France, 2024."},{"key":"7_CR28","doi-asserted-by":"crossref","unstructured":"Paulo\u00a0Em\u00edlio de\u00a0Vilhena and Fran\u00e7ois Pottier. A separation logic for effect handlers. Proc. ACM Program. Lang., 5(POPL), January 2021.","DOI":"10.1145\/3434314"},{"key":"7_CR29","doi-asserted-by":"crossref","unstructured":"Pablo Donato, Pierre-Yves Strub, and Benjamin Werner. A drag-and-drop proof tactic. In Andrei Popescu and Steve Zdancewic, editors, CPP \u201922: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022, pages 197\u2013209. ACM, 2022.","DOI":"10.1145\/3497775.3503692"},{"key":"7_CR30","unstructured":"Catherine Dubois, Nicolas Magaud, and Alain Giorgetti. Pragmatic isomorphism proofs between coq representations: Application to lambda-term families. In Delia Kesner and Pierre-Marie P\u00e9drot, editors, 28th International Conference on Types for Proofs and Programs, TYPES 2022, June 20-25, 2022, LS2N, University of Nantes, France, volume 269 of LIPIcs, pages 11:1\u201311:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2022."},{"key":"7_CR31","doi-asserted-by":"crossref","unstructured":"Cvetan Dunchev, Ferruccio Guidi, Claudio\u00a0Sacerdoti Coen, and Enrico Tassi. ELPI: fast, embeddable, $$\\lambda $$prolog interpreter. In Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings, volume 9450 of Lecture Notes in Computer Science, pages 460\u2013468. Springer, 2015.","DOI":"10.1007\/978-3-662-48899-7_32"},{"key":"7_CR32","doi-asserted-by":"crossref","unstructured":"Gabriel Ebner, Sebastian Ullrich, Jared Roesch, Jeremy Avigad, and Leonardo de\u00a0Moura. A metaprogramming framework for formal verification. Proc. ACM Program. Lang., 1(ICFP), August 2017.","DOI":"10.1145\/3110278"},{"key":"7_CR33","unstructured":"Davide Fissore and Enrico Tassi. A new Type-Class solver for Coq in Elpi. In The Coq Workshop 2023, Bialystok, Poland, July 2023."},{"key":"7_CR34","unstructured":"Jo\u00e3o Paulo\u00a0Pizani Flor, Wouter Swierstra, and Yorick Sijsling. Pi-ware: Hardware description and verification in agda. In Tarmo Uustalu, editor, 21st International Conference on Types for Proofs and Programs, TYPES 2015, May 18-21, 2015, Tallinn, Estonia, volume\u00a069 of LIPIcs, pages 9:1\u20139:27. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2015."},{"key":"7_CR35","doi-asserted-by":"crossref","unstructured":"Yannick Forster, Matthieu Sozeau, and Nicolas Tabareau. Verified extraction from coq to ocaml. Proc. ACM Program. Lang., 8(PLDI), June 2024.","DOI":"10.1145\/3656379"},{"key":"7_CR36","doi-asserted-by":"crossref","unstructured":"Yannick Forster and Kathrin Stark. Coq \u00e0 la carte: a practical approach to modular syntax with binders. In Jasmin Blanchette and Catalin Hritcu, editors, Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020, pages 186\u2013200. ACM, 2020.","DOI":"10.1145\/3372885.3373817"},{"key":"7_CR37","doi-asserted-by":"crossref","unstructured":"Andrew Gacek. The abella interactive theorem prover (system description). In Proceedings of the 4th International Joint Conference on Automated Reasoning (IJCAR), pages 154\u2013161. Springer, 2008.","DOI":"10.1007\/978-3-540-71070-7_13"},{"key":"7_CR38","doi-asserted-by":"crossref","unstructured":"Benjamin Gr\u00e9goire, Jean-Christophe L\u00e9chenet, and Enrico Tassi. Practical and sound equality tests, automatically \u2013 Deriving eqType instances for Jasmin\u2019s data types with Coq-Elpi. In CPP 2023: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023: Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 167\u2013181, Boston MA USA, France, January 2023. ACM.","DOI":"10.1145\/3573105.3575683"},{"key":"7_CR39","unstructured":"Jason Gross, Th\u00e9o Zimmermann, Miraya Poddar-Agrawal, and Adam Chlipala. Automatic test-case reduction in proof assistants: A case study in coq. In June Andronick and Leonardo de\u00a0Moura, editors, 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel, volume 237 of LIPIcs, pages 18:1\u201318:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2022."},{"key":"7_CR40","doi-asserted-by":"crossref","unstructured":"Ferruccio Guidi, Claudio Sacerdoti\u00a0Coen, and Enrico Tassi. Implementing Type Theory in Higher Order Constraint Logic Programming. Mathematical Structures in Computer Science, 29(8):1125\u20131150, March 2019.","DOI":"10.1017\/S0960129518000427"},{"key":"7_CR41","unstructured":"Hugo Herbelin. reduction-effects."},{"key":"7_CR42","doi-asserted-by":"crossref","unstructured":"Jason Z.\u00a0S. Hu and Brigitte Pientka. A layered approach to intensional analysis in type theory. ACM Trans. Program. Lang. Syst., 46(4):15:1\u201315:43, 2024.","DOI":"10.1145\/3707203"},{"key":"7_CR43","doi-asserted-by":"crossref","unstructured":"Jason Z.\u00a0S. Hu and Brigitte Pientka. Layered modal type theory - where meta-programming meets intensional analysis. In Stephanie Weirich, editor, Programming Languages and Systems - 33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I, volume 14576 of Lecture Notes in Computer Science, pages 52\u201382. Springer, 2024.","DOI":"10.1007\/978-3-031-57262-3_3"},{"key":"7_CR44","doi-asserted-by":"crossref","unstructured":"Jason Z.\u00a0S. Hu and Brigitte Pientka. A dependent type theory for meta-programming with intensional analysis. Proc. ACM Program. Lang., 9(POPL):416\u2013445, 2025.","DOI":"10.1145\/3704851"},{"key":"7_CR45","doi-asserted-by":"crossref","unstructured":"Jason Z.\u00a0S. Hu, Brigitte Pientka, and Ulrich Sch\u00f6pp. A category theoretic view of contextual types: From simple types to dependent types. ACM Trans. Comput. Log., 23(4):25:1\u201325:36, 2022.","DOI":"10.1145\/3545115"},{"key":"7_CR46","doi-asserted-by":"crossref","unstructured":"Junyoung Jang, Samuel G\u00e9lineau, Stefan Monnier, and Brigitte Pientka. M\u0153bius: metaprogramming using contextual types: the stage where system f can pattern match on itself. Proc. ACM Program. Lang., 6(POPL):1\u201327, 2022.","DOI":"10.1145\/3498700"},{"key":"7_CR47","doi-asserted-by":"crossref","unstructured":"Th\u00e9o Laurent, Meven Lennon-Bertrand, and Kenji Maillard. Definitional functoriality for dependent (Sub)Types. In Lecture Notes in Computer Science, pages 302\u2013331. 2024.","DOI":"10.1007\/978-3-031-57262-3_13"},{"key":"7_CR48","unstructured":"Bohdan Liesnikov, Marcel Ullrich, and Yannick Forster. Generating induction principles and subterm relations for inductive types using metacoq. CoRR, abs\/2006.15135, 2020."},{"key":"7_CR49","doi-asserted-by":"crossref","unstructured":"Jannis Limperg. A novice-friendly induction tactic for lean. In Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, page 199\u2013211, New York, NY, USA, 2021. Association for Computing Machinery.","DOI":"10.1145\/3437992.3439928"},{"key":"7_CR50","doi-asserted-by":"crossref","unstructured":"Jannis Limperg and Asta\u00a0Halkj\u00e6r From. Aesop: White-box best-first proof search for lean. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, page 253\u2013266, New York, NY, USA, 2023. Association for Computing Machinery.","DOI":"10.1145\/3573105.3575671"},{"key":"7_CR51","doi-asserted-by":"crossref","unstructured":"Nicolas Magaud. Towards automatic transformations of coq proof scripts. In Pedro Quaresma and Zolt\u00e1n Kov\u00e1cs, editors, Proceedings 14th International Conference on Automated Deduction in Geometry, ADG 2023, Belgrade, Serbia, 20-22th September 2023, volume 398 of EPTCS, pages 4\u201310, 2023.","DOI":"10.4204\/EPTCS.398.4"},{"key":"7_CR52","doi-asserted-by":"crossref","unstructured":"Kenji Maillard, Danel Ahman, Robert Atkey, Guido Mart\u00ednez, C\u0103t\u0103lin Hri\u0163cu, Exequiel Rivas, and \u00c9ric Tanter. Dijkstra monads for all. Proc. ACM Program. Lang., 3(ICFP), July 2019.","DOI":"10.1145\/3341708"},{"key":"7_CR53","doi-asserted-by":"crossref","unstructured":"Kenji Maillard, C\u0103t\u0103lin Hri\u0163cu, Exequiel Rivas, and Antoine Van\u00a0Muylder. The next 700 relational program logics. Proc. ACM Program. Lang., 4(POPL), December 2019.","DOI":"10.1145\/3371072"},{"key":"7_CR54","unstructured":"Matteo Manighetti, Dale Miller, and Alberto Momigliano. Two Applications of Logic Programming to Coq. In Ugo de\u2019Liguoro, Stefano Berardi, and Thorsten Altenkirch, editors, 26th International Conference on Types for Proofs and Programs (TYPES 2020), volume 188 of Leibniz International Proceedings in Informatics (LIPIcs), pages 10:1\u201310:19, Dagstuhl, Germany, 2021. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik."},{"key":"7_CR55","doi-asserted-by":"crossref","unstructured":"The mathlib Community. The lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, page 367\u2013381, New York, NY, USA, 2020. Association for Computing Machinery.","DOI":"10.1145\/3372885.3373824"},{"key":"7_CR56","doi-asserted-by":"crossref","unstructured":"Leonardo\u00a0de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In Lecture Notes in Computer Science, pages 625\u2013635. 2021.","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"7_CR57","doi-asserted-by":"crossref","unstructured":"Leonardo\u00a0de Moura and Sebastian Ullrich. The lean 4 theorem prover and programming language. In Andr\u00e9 Platzer and Geoff Sutcliffe, editors, Automated Deduction \u2013 CADE 28, pages 625\u2013635, Cham, 2021. Springer International Publishing.","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"7_CR58","unstructured":"Gopalan Nadathur and Dale Miller. An overview of lambda prolog. Technical report, USA, 1988."},{"key":"7_CR59","unstructured":"Wojciech Nawrocki, Edward\u00a0W. Ayers, and Gabriel Ebner. An extensible user interface for lean 4. In Adam Naumowicz and Ren\u00e9 Thiemann, editors, 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Bia\u0142ystok, Poland, volume 268 of LIPIcs, pages 24:1\u201324:20. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2023."},{"key":"7_CR60","unstructured":"Pierre Nigron and Pierre-\u00c9variste Dagand. Reaching for the Star: Tale of a Monad in Coq. In Leibniz International Proceedings in Informatics (LIPIcs), volume 193 of Leibniz International Proceedings in Informatics (LIPIcs), pages 29:1\u201329:19, Rome, Italy, June 2021. Schloss Dagstuhl."},{"key":"7_CR61","unstructured":"Ulf Norell. agda-prelude: Programming library for agda."},{"key":"7_CR62","unstructured":"Ulf Norell. Towards a practical programming language based on dependent type theory, volume\u00a032. Chalmers University of Technology, 2007."},{"key":"7_CR63","unstructured":"Ulf Norell, Nils\u00a0Anders Danielsson, Jesper Cockx, and Andreas Abel. Agda wiki. http:\/\/wiki.portal.chalmers.se\/agda\/pmwiki.php."},{"key":"7_CR64","doi-asserted-by":"crossref","unstructured":"Zoe Paraskevopoulou, Aaron Eline, and Leonidas Lampropoulos. Computing correctly with inductive relations. In Ranjit Jhala and Isil Dillig, editors, PLDI \u201922: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13 - 17, 2022, pages 966\u2013980. ACM, 2022.","DOI":"10.1145\/3519939.3523707"},{"key":"7_CR65","doi-asserted-by":"crossref","unstructured":"Christine Paulin-Mohring. Inductive definitions in the system Coq rules and properties. In International Conference on Typed Lambda Calculi and Applications, pages 328\u2013345. Springer, 1993.","DOI":"10.1007\/BFb0037116"},{"key":"7_CR66","unstructured":"Arthur Paulino, D\u00a0Testa, E\u00a0Ayers, H\u00a0B\u00f6ving, J\u00a0Limperg, S\u00a0Gadgil, and S\u00a0Bhat. Metaprogramming in lean 4. Online Book. https:\/\/github.com\/arthurpaulino\/lean4-metaprogramming-book, 2024."},{"key":"7_CR67","doi-asserted-by":"crossref","unstructured":"F.\u00a0Pfenning and C.\u00a0Elliott. Higher-order abstract syntax. SIGPLAN Not., 23(7):199\u2013208, June 1988.","DOI":"10.1145\/960116.54010"},{"key":"7_CR68","doi-asserted-by":"crossref","unstructured":"Brigitte Pientka. A type-theoretic framework for certified meta-programming (invited talk extended abstract). In Guillaume Allais and Yanhong\u00a0Annie Liu, editors, Proceedings of the 2025 ACM SIGPLAN International Workshop on Partial Evaluation and Program Manipulation, PEPM 2025, Denver, CO, USA, 21 January 2025, pages 10\u201311. ACM, 2025.","DOI":"10.1145\/3704253.3706136"},{"key":"7_CR69","doi-asserted-by":"crossref","unstructured":"Brigitte Pientka and Joshua Dunfield. Beluga: A framework for programming and reasoning with contextual data. In Proceedings of the 10th International Symposium on Functional and Logic Programming (FLOPS), pages 1\u201317. Springer, 2010.","DOI":"10.1007\/978-3-642-12251-4_1"},{"key":"7_CR70","doi-asserted-by":"crossref","unstructured":"Gordon\u00a0D. Plotkin and Matija Pretnar. Handling algebraic effects. Log. Methods Comput. Sci., 9, 2013.","DOI":"10.2168\/LMCS-9(4:23)2013"},{"key":"7_CR71","unstructured":"Pierre-Marie P\u00e9drot. Ltac2: Tactical warfare. In The 5th International Workshop on Coq for Programming Languages (CoqPL 2019), 2019. Talk at CoqPL 2019, affiliated with POPL 2019."},{"key":"7_CR72","unstructured":"Talia Ringer. Proof Repair. PhD thesis, University of Washington, USA, 2021."},{"key":"7_CR73","doi-asserted-by":"crossref","unstructured":"Ayumu Saito and Reynald Affeldt. Towards a practical library for monadic equational reasoning in coq. In Ekaterina Komendantskaya, editor, Mathematics of Program Construction, pages 151\u2013177, Cham, 2022. Springer International Publishing.","DOI":"10.1007\/978-3-031-16912-0_6"},{"key":"7_CR74","unstructured":"Kazuhiko Sakaguchi. Reflexive tactics for algebra, revisited. In June Andronick and Leonardo de\u00a0Moura, editors, 13th International Conference on Interactive Theorem Proving, ITP 2022, August 7-10, 2022, Haifa, Israel, volume 237 of LIPIcs, pages 29:1\u201329:22. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2022."},{"key":"7_CR75","doi-asserted-by":"crossref","unstructured":"Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, and Th\u00e9o Winterhalter. The MetaCoq Project. Journal of Automated Reasoning, February 2020.","DOI":"10.1007\/s10817-019-09540-0"},{"key":"7_CR76","doi-asserted-by":"crossref","unstructured":"Matthieu Sozeau, Simon Boulier, Yannick Forster, Nicolas Tabareau, and Th\u00e9o Winterhalter. Coq coq correct! verification of type checking and erasure for coq, in coq. Proc. ACM Program. Lang., 4(POPL), December 2019.","DOI":"10.1145\/3371076"},{"key":"7_CR77","doi-asserted-by":"crossref","unstructured":"Kathrin Stark, Steven Sch\u00e4fer, and Jonas Kaiser. Autosubst 2: reasoning with multi-sorted de bruijn terms and vector substitutions. In Assia Mahboubi and Magnus\u00a0O. Myreen, editors, Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, Cascais, Portugal, January 14-15, 2019, pages 166\u2013180. ACM, 2019.","DOI":"10.1145\/3293880.3294101"},{"key":"7_CR78","doi-asserted-by":"crossref","unstructured":"Carst Tankink, Herman Geuvers, James McKinna, and Freek Wiedijk. Proviola: A tool for proof re-animation. CoRR, abs\/1005.2672, 2010.","DOI":"10.1007\/978-3-642-14128-7_37"},{"key":"7_CR79","unstructured":"Enrico Tassi. Deriving Proved Equality Tests in Coq-Elpi: Stronger Induction Principles for Containers in Coq. In John Harrison, John O\u2019Leary, and Andrew Tolmach, editors, 10th International Conference on Interactive Theorem Proving (ITP 2019), volume 141 of Leibniz International Proceedings in Informatics (LIPIcs), pages 29:1\u201329:18, Dagstuhl, Germany, 2019. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik."},{"key":"7_CR80","unstructured":"The Coq Development Team. The coq proof assistant, September 2024."},{"key":"7_CR81","doi-asserted-by":"crossref","unstructured":"Sebastian Ullrich and Leonardo de\u00a0Moura. Beyond notations: Hygienic macro expansion for theorem proving languages. In Automated Reasoning: 10th International Joint Conference, IJCAR 2020, Paris, France, July 1\u20134, 2020, Proceedings, Part II, page 167\u2013182, Berlin, Heidelberg, 2020. Springer-Verlag.","DOI":"10.1007\/978-3-030-51054-1_10"},{"key":"7_CR82","doi-asserted-by":"crossref","unstructured":"Sebastian Ullrich and Leonardo de\u00a0Moura. \u2018do\u2019 unchained: embracing local imperativity in a purely functional language (functional pearl). Proc. ACM Program. Lang., 6(ICFP), August 2022.","DOI":"10.1145\/3547640"},{"key":"7_CR83","doi-asserted-by":"crossref","unstructured":"Cas van\u00a0der Rest and Wouter Swierstra. A completely unique account of enumeration. Proc. ACM Program. Lang., 6(ICFP):411\u2013437, 2022.","DOI":"10.1145\/3547636"},{"key":"7_CR84","doi-asserted-by":"crossref","unstructured":"Paul van\u00a0der Walt and Wouter Swierstra. Engineering proof by reflection in agda. In International Symposium on Implementation and Application of Functional Languages, 2012.","DOI":"10.1007\/978-3-642-41582-1_10"},{"key":"7_CR85","doi-asserted-by":"crossref","unstructured":"Marcell van Geest and Wouter Swierstra. Generic packet descriptions: verified parsing and pretty printing of low-level data. In Sam Lindley and Brent\u00a0A. Yorgey, editors, Proceedings of the 2nd ACM SIGPLAN International Workshop on Type-Driven Development, TyDe@ICFP 2017, Oxford, UK, September 3, 2017, pages 30\u201340. ACM, 2017.","DOI":"10.1145\/3122975.3122979"},{"key":"7_CR86","doi-asserted-by":"crossref","unstructured":"Max Vistrup, Michael Sammler, and Ralf Jung. Program logics \u00e0 la carte. Proc. ACM Program. Lang., 9(POPL), January 2025.","DOI":"10.1145\/3704847"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-22720-1_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T19:24:40Z","timestamp":1777577080000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22720-1_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227195","9783032227201"],"references-count":86,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22720-1_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"10 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Turin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"35","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/about\/esop\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}