Extensible and Efficient Automation Through Reflective Tactics
No abstract available.
Related papers
- Verified and Optimized Implementation of Orthologic Proof Search CAV 2025
- Mtac: A monad for typed tactic programming in Coq JFP 2015
- Meta-F ^\star : Proof Automation with SMT, Tactics, and Metaprograms ESOP 2019
- A metaprogramming framework for formal verification ICFP 2017
- MoSeL: a general, extensible modal framework for interactive proofs in separation logic ICFP 2018
- Automated Discovery of Tactic Libraries for Interactive Theorem Proving OOPSLA 2025
- Mtac: a monad for typed tactic programming in Coq ICFP 2013
- A Lambda-Superposition Tactic for Isabelle/HOL CPP 2026