Code Generation via Meta-programming in Dependently Typed Proof Assistants
summary
A survey implements seven implementations of a Functor-deriving meta program that generates the map function for option/list/tree and other boilerplate across Coq (OCaml plugins, MetaCoq, Ltac2, Elk, LP) Agda and Lean. Results show OCaml plugins force low-level AST work and use de Bruijn indices that are error-prone, MetaCoq/Agda have quoting and state limits, Ltac2 is ergonomic but hard to reason about, LP and Lean feel pleasant but Lean’s fixed-point/recursor support leaves its implementation incomplete; code and preprint are on GitHub and the ISOP paper.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 3:01Meta-programming frameworks in Rock
- 5:30Okamel plugins for low-level meta
- 8:00Metarok as Rock programs
- 9:25Agda's reflection API
- 11:32Eltech 2 tactics
- 13:58Lean's meta-programming
- 16:26Comparative analysis
- 18:14Future work
- 21:56Q&A
related talks
22mInducTeX: A MetaCoq plugin for typesetting inductive definitions
07h 18mFull Workshop
16mWe’ve Got You Covered: Type-Guided Repair of Incomplete Input Generators
42mBecoming the Metaprogrammer Real World Code Generation
01h 10mMedium-scale automation for proof assistants
21mLive Verification in an Interactive Proof Assistant
37mThings I learned after a decade of writing code generators
27mParsing, Compiling, and Static Metaprogramming