Mtac
From MaRDI portal
swMATH13075MaRDI QIDQ24994FDOQ24994
Author name not available (Why is that?)
Official website: http://dl.acm.org/citation.cfm?doid=2500365.2500579
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
- A unification algorithm for Coq featuring universe polymorphism and overloading
- Rtac
- VeriML
- Mtac: a monad for typed tactic programming in Coq
- Tactics and certificates in Meta Dedukti
- Elaborator reflection: extending Idris in Idris
- Idris
- CertiKOS
- Calcite
- CertiCoq
- Hazelnut
- js_of_ocaml
- Lamdu
- mbeddr
- TouchDevelop
- Gallina
- Template-Coq
- HOL Light QE
- Meta Dedukti
- GeoCoq
- SerAPI
- A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
- Hazelnut: a bidirectionally typed structure editor calculus
- A Why3 framework for reflection proofs and its application to GMP's algorithms
- MetaCoq
- Harpoon
- Extensible and efficient automation through reflective tactics
- Harpoon: mechanizing metatheory interactively
- Towards certified meta-programming with typed Template-Coq
This page was built for software: Mtac
