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