×

Mtac

swMATH ID: 13075
Software Authors: Ziliani, Beta; Dreyer, Derek; Krishnaswami, Neelakantan R.; Nanevski, Aleksandar; Vafeiadis, Viktor
Description: 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.
Homepage: http://dl.acm.org/citation.cfm?doid=2500365.2500579
Dependencies: Coq
Keywords: Coq; custom proof automation; interactive theorem proving; monads; tactics; typed meta-programming
Related Software: Coq; Agda; Idris; seL4; VeriML; HOL; Isabelle; LCF; Isabelle/HOL; Gallina; Template-Coq; CertiCoq; Irdis; kepler98; Lean; Zoo Probabilistic Systems; Eisbach; Locales; Coq/SSReflect; Beluga
Cited in: 16 Publications

Standard Articles

1 Publication describing the Software, including 1 Publication in zbMATH Year
Mtac: a monad for typed tactic programming in Coq. Zbl 1323.68236
Ziliani, Beta; Dreyer, Derek; Krishnaswami, Neelakantan R.; Nanevski, Aleksandar; Vafeiadis, Viktor
2013
all top 5

Cited by 35 Authors

5 Ziliani, Beta
4 Sozeau, Matthieu
2 Anand, Abhishek
2 Boulier, Simon
2 Brady, Edwin C.
2 Cohen, Cyril
2 Dreyer, Derek R.
2 Krishnaswami, Neelakantan R.
2 Malecha, Gregory
2 Nanevski, Aleksandar
2 Tabareau, Nicolas
2 Vafeiadis, Viktor
1 Aldrich, Jonathan
1 Bengtson, Jesper
1 Cauderlier, Raphaël
1 Christiansen, David R.
1 Errington, Jacob
1 Fervari, Raul
1 Forster, Yannick
1 Hammer, Matthew A.
1 Jang, Junyoung
1 Kokke, Pepijn
1 Kunze, Fabian
1 Matichuk, Daniel
1 Melquiond, Guillaume
1 Murray, Toby
1 Omar, Cyrus
1 Pientka, Brigitte
1 Rieu-Helft, Raphaël
1 Slama, Franck
1 Swierstra, Wouter
1 Trucco, Francisco
1 Voysey, Ian
1 Wenzel, Makarius
1 Winterhalter, Théo

Cited in 3 Serials

2 Journal of Automated Reasoning
2 Journal of Functional Programming
1 Journal of Logical and Algebraic Methods in Programming

Cited in 2 Fields

16 Computer science (68-XX)
2 Mathematical logic and foundations (03-XX)

Citations by Year