Mtac
From MaRDI portal
Cited in
(34)- Auto in Agda. Programming proof search using reflection
- Elaborator reflection: extending Idris in Idris
- Eisbach: a proof method language for Isabelle
- Extensible and efficient automation through reflective tactics
- Verification of dynamic bisimulation theorems in Coq
- Automatically proving equivalence by type-safe reflection
- Harpoon: mechanizing metatheory interactively
- Rtac
- VeriML
- A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
- A unification algorithm for Coq featuring universe polymorphism and overloading
- Idris
- CertiKOS
- Calcite
- CertiCoq
- Hazelnut
- js_of_ocaml
- Lamdu
- mbeddr
- TouchDevelop
- Gallina
- Template-Coq
- HOL Light QE
- Meta Dedukti
- GeoCoq
- SerAPI
- MetaCoq
- Mtac: a monad for typed tactic programming in Coq
- Hazelnut: a bidirectionally typed structure editor calculus
- A Why3 framework for reflection proofs and its application to GMP's algorithms
- Harpoon
- Tactics and certificates in Meta Dedukti
- The \textsc{MetaCoq} project
- Towards certified meta-programming with typed Template-Coq
This page was built for software: Mtac
