Mtac

DOI10.1145/2500365.2500579zbMath1323.68236OpenAlexW2160230109MaRDI QIDQ5244791

Viktor Vafeiadis, Aleksandar Nanevski, Derek R. Dreyer, Neelakantan R. Krishnaswami, Beta Ziliani

Publication date: 30 March 2015

Published in: Proceedings of the 18th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/2500365.2500579

zbMATH Keywords

monadsinteractive theorem provingCoqtacticscustom proof automationtyped meta-programming

Mathematics Subject Classification ID

Related Items (7)

Automatically proving equivalence by type-safe reflection ⋮ Eisbach: a proof method language for Isabelle ⋮ Auto in Agda ⋮ Mtac: A monad for typed tactic programming in Coq ⋮ A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading ⋮ Extensible and Efficient Automation Through Reflective Tactics ⋮ Mtac

Uses Software

• Coq
• VeriML

This page was built for publication: Mtac