Mtac

swMATH13075MaRDI QIDQ24994FDOQ24994

Author name not available (Why is that?)

Described by source

• Mtac

Cited In (15)

• Verification of dynamic bisimulation theorems in Coq
• The \textsc{MetaCoq} project
• Extensible and Efficient Automation Through Reflective Tactics
• Mtac: A monad for typed tactic programming in Coq
• Eisbach: a proof method language for Isabelle
• Automatically proving equivalence by type-safe reflection
• A unification algorithm for Coq featuring universe polymorphism and overloading
• Auto in Agda
• Tactics and certificates in Meta Dedukti
• Elaborator reflection: extending Idris in Idris
• 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
• Harpoon: mechanizing metatheory interactively
• Towards certified meta-programming with typed Template-Coq

This page was built for software: Mtac