Mtac

Mtac: a monad for typed tactic programming in Coq. Effective support for custom proof automation is essential for large scale interactive proof development. However, existing languages for automation via tactics either (a) provide no way to specify the behavior of tactics within the base logic of the accompanying theorem prover, or (b) rely on advanced type-theoretic machinery that is not easily integrated into established theorem provers.par We present Mtac, a lightweight but powerful extension to Coq that supports dependently-typed tactic programming. Mtac tactics have access to all the features of ordinary Coq programming, as well as a new set of typed tactical primitives. We avoid the need to touch the trusted kernel typechecker of Coq by encapsulating uses of these new tactical primitives in a monad, and instrumenting Coq so that it executes monadic tactics during type inference.

This software is also peer reviewed by journal TOMS.


References in zbMATH (referenced in 14 articles , 1 standard article )

Showing results 1 to 14 of 14.
Sorted by year (citations)

  1. Sozeau, Matthieu; Anand, Abhishek; Boulier, Simon; Cohen, Cyril; Forster, Yannick; Kunze, Fabian; Malecha, Gregory; Tabareau, Nicolas; Winterhalter, Théo: The \textscMetaCoqproject (2020)
  2. Anand, Abhishek; Boulier, Simon; Cohen, Cyril; Sozeau, Matthieu; Tabareau, Nicolas: Towards certified meta-programming with typed Template-Coq (2018)
  3. Cauderlier, Raphaël: Tactics and certificates in Meta Dedukti (2018)
  4. Melquiond, Guillaume; Rieu-Helft, Raphaël: A Why3 framework for reflection proofs and its application to GMP’s algorithms (2018)
  5. Omar, Cyrus; Voysey, Ian; Hilton, Michael; Aldrich, Jonathan; Hammer, Matthew A.: Hazelnut: a bidirectionally typed structure editor calculus (2017)
  6. Slama, Franck; Brady, Edwin: Automatically proving equivalence by type-safe reflection (2017)
  7. Ziliani, Beta; Sozeau, Matthieu: A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading (2017)
  8. Christiansen, David; Brady, Edwin: Elaborator reflection: extending Idris in Idris (2016)
  9. Malecha, Gregory; Bengtson, Jesper: Extensible and efficient automation through reflective tactics (2016)
  10. Matichuk, Daniel; Murray, Toby; Wenzel, Makarius: Eisbach: a proof method language for Isabelle (2016)
  11. Kokke, Pepijn; Swierstra, Wouter: Auto in Agda. Programming proof search using reflection (2015)
  12. Ziliani, Beta; Dreyer, Derek; Krishnaswami, Neelakantan R.; Nanevski, Aleksandar; Vafeiadis, Viktor: Mtac: a monad for typed tactic programming in Coq (2015)
  13. Ziliani, Beta; Sozeau, Matthieu: A unification algorithm for Coq featuring universe polymorphism and overloading (2015)
  14. Ziliani, Beta; Dreyer, Derek; Krishnaswami, Neelakantan R.; Nanevski, Aleksandar; Vafeiadis, Viktor: Mtac: a monad for typed tactic programming in Coq (2013)