The following pages link to Mtac (Q24994):
Displaying 15 items.
- Eisbach: a proof method language for Isabelle (Q287365) (← links)
- Towards certified meta-programming with typed Template-Coq (Q1791140) (← links)
- Tactics and certificates in Meta Dedukti (Q1791152) (← links)
- A Why3 framework for reflection proofs and its application to GMP's algorithms (Q1799078) (← links)
- Verification of dynamic bisimulation theorems in Coq (Q2035655) (← links)
- Harpoon: mechanizing metatheory interactively (Q2055903) (← links)
- The \textsc{MetaCoq} project (Q2209542) (← links)
- Automatically proving equivalence by type-safe reflection (Q2364699) (← links)
- Extensible and Efficient Automation Through Reflective Tactics (Q2802496) (← links)
- Auto in Agda (Q2941181) (← links)
- A unification algorithm for Coq featuring universe polymorphism and overloading (Q2981954) (← links)
- Elaborator reflection: extending Idris in Idris (Q2985777) (← links)
- Hazelnut: a bidirectionally typed structure editor calculus (Q5370848) (← links)
- Mtac: A monad for typed tactic programming in Coq (Q5371944) (← links)
- A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading (Q5372007) (← links)
