Monadic typed tactic programming by reflection
summary
Shallow embedding of Mtac is implemented entirely in Agda by reusing Agda reflection and quotations to represent tactic terms as Agda syntax; the implementation realizes 12 of 13 constructs (pattern matching, binders, local names, failure) with each nontrivial construct implemented in roughly ten lines and one recursive primitive left out. Key issues are universe/level management for quoted terms, alpha‑equivalence and unquote soundness assumptions, and some unproven coherence lemmas; a small demo runs in seconds.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:58What is Monadic
- 5:53Personal semantics
- 6:30Reflection
- 8:17Limitations
- 10:49Syntax
- 12:39Unification
- 15:45Extractions
- 16:25Proof
- 22:21Problems
related talks
24mGeneralization of meta programs with dependent types in mtac2 with mtac2
25mShallowly embedding type theories
15mMonadification of Attribute Grammars
14mType-Sensitive Algebraic Macros
56mOn Type-Based Techniques for Program Manipulation
20mA Dependent Type Theory for Meta-programming with Intensional Analysis
29mMechanized monadic equational reasoning for ML references
42mFunctional interpreters and you