{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:43:05Z","timestamp":1770284585177,"version":"3.49.0"},"reference-count":52,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2015,8,24]],"date-time":"2015-08-24T00:00:00Z","timestamp":1440374400000},"content-version":"unspecified","delay-in-days":235,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2015]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Effective support for custom proof automation is essential for large-scale interactive proof development. However, existing languages for automation via <jats:italic>tactics<\/jats:italic> 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.<\/jats:p><jats:p>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 <jats:italic>monad<\/jats:italic>, and instrumenting Coq so that it executes monadic tactics during type inference.<\/jats:p>","DOI":"10.1017\/s0956796815000118","type":"journal-article","created":{"date-parts":[[2015,8,24]],"date-time":"2015-08-24T07:21:01Z","timestamp":1440400861000},"source":"Crossref","is-referenced-by-count":16,"title":["Mtac: A monad for typed tactic programming in Coq"],"prefix":"10.1017","volume":"25","author":[{"given":"BETA","family":"ZILIANI","sequence":"first","affiliation":[]},{"given":"DEREK","family":"DREYER","sequence":"additional","affiliation":[]},{"given":"NEELAKANTAN R.","family":"KRISHNASWAMI","sequence":"additional","affiliation":[]},{"given":"ALEKSANDAR","family":"NANEVSKI","sequence":"additional","affiliation":[]},{"given":"VIKTOR","family":"VAFEIADIS","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2015,8,24]]},"reference":[{"key":"S0956796815000118_ref10","volume-title":"Certified Programming with Dependent Types","author":"Chlipala","year":"2011"},{"key":"S0956796815000118_ref48","doi-asserted-by":"crossref","unstructured":"Stampoulis A. & Shao Z. (2012) Static and user-extensible proof checking. In ACM Symposium on Principles of Programming Languages (POPL). New York: ACM.","DOI":"10.1145\/2103656.2103690"},{"key":"S0956796815000118_ref45","unstructured":"Sozeau M. (2007) Subset coercions in Coq. In TYPES. Berlin: Springer."},{"key":"S0956796815000118_ref42","doi-asserted-by":"crossref","unstructured":"Sa\u00efbi A. (1997) Typing algorithm in type theory with inheritance. In ACM Symposium on Principles of Programming Languages (POPL). New York: ACM.","DOI":"10.1145\/263699.263742"},{"key":"S0956796815000118_ref33","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006953"},{"key":"S0956796815000118_ref52","doi-asserted-by":"crossref","unstructured":"Ziliani B. , Dreyer D. , Krishnaswami N. R. , Nanevski A. & Vafeiadis V. (2013) Mtac: A monad for typed tactic programming in Coq. In International Conference on Functional Programming (ICFP). New York: ACM.","DOI":"10.1145\/2500365.2500579"},{"key":"S0956796815000118_ref16","doi-asserted-by":"crossref","unstructured":"Gonthier G. , Asperti A. , Avigad J. , Bertot Y. , Cohen C. , Garillot F. , LeRoux S. , Mahboubi A. , O'Connor R. , Ould Biha S. , Pasca I. , Rideau L. , Solovyev A. , Tassi E. & Th\u00e9ry L. (2013b) A machine-checked proof of the odd order theorem. In International Conference on Interactive Theorem Proving (ITP). Berlin: Springer.","DOI":"10.1007\/978-3-642-39634-2_14"},{"key":"S0956796815000118_ref28","doi-asserted-by":"crossref","unstructured":"Malecha G. , Chlipala A. & Braibant T. (2014) Compositional computational reflection. In International Conference on Interactive Theorem Proving (ITP). Berlin: Springer.","DOI":"10.1007\/978-3-319-08970-6_24"},{"key":"S0956796815000118_ref27","unstructured":"Malecha G. & Bengtson J. (2015) Rtac: A fully reflective tactic language. In International Workshop on Coq for PL (CoqPL)."},{"key":"S0956796815000118_ref25","doi-asserted-by":"crossref","unstructured":"Launchbury J. & Peyton Jones S. L. (1994) Lazy functional state threads. In ACM Conference on Programming Languages Design and Implementation (PLDI). New York: ACM.","DOI":"10.1145\/178243.178246"},{"key":"S0956796815000118_ref26","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"S0956796815000118_ref24","doi-asserted-by":"publisher","DOI":"10.1145\/1743546.1743574"},{"key":"S0956796815000118_ref23","doi-asserted-by":"crossref","unstructured":"Hur C.-K. , Neis G. , Dreyer D. & Vafeiadis V. (2013) The power of parameterization in coinductive proof. In ACM Symposium on Principles of Programming Languages (POPL). New York: ACM.","DOI":"10.1145\/2429069.2429093"},{"key":"S0956796815000118_ref8","doi-asserted-by":"crossref","unstructured":"Boutin S. (1997) Using reflection to build efficient and certified decision procedures. In International Symposium on Theoretical Aspects of Computer Software (TACS). Berlin: Springer.","DOI":"10.1007\/BFb0014565"},{"key":"S0956796815000118_ref5","doi-asserted-by":"publisher","DOI":"10.1145\/122598.122614"},{"key":"S0956796815000118_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/s12046-009-0003-3"},{"key":"S0956796815000118_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"S0956796815000118_ref3","doi-asserted-by":"crossref","unstructured":"Art\u00ebmov S. N. (1999) On explicit reflection in theorem proving and formal verification. In Conference on Automated Deduction (CADE). Berlin: Springer.","DOI":"10.1007\/3-540-48660-7_23"},{"key":"S0956796815000118_ref47","doi-asserted-by":"crossref","unstructured":"Stampoulis A. & Shao Z. (2010) VeriML: Typed computation of logical terms inside a language with effects. In International Conference on Functional Programming (ICFP). New York: ACM.","DOI":"10.1145\/1863543.1863591"},{"key":"S0956796815000118_ref19","doi-asserted-by":"crossref","unstructured":"Gr\u00e9goire B. & Leroy X. (2002) A compiled implementation of strong reduction. In International Conference on Functional Programming (ICFP). New York: ACM.","DOI":"10.1145\/581478.581501"},{"key":"S0956796815000118_ref31","unstructured":"Miller D. (1991) Unification of simply typed lamda-terms as logic programming. In International Conference on Logic Programming (ICLP). Berlin: Springer."},{"key":"S0956796815000118_ref9","doi-asserted-by":"crossref","unstructured":"Cave A. & Pientka B. (2012) Programming with binders and indexed data-types. In ACM Symposium on Principles of Programming Languages (POPL). New York: ACM.","DOI":"10.1145\/2103656.2103705"},{"key":"S0956796815000118_ref35","first-page":"23:1","article-title":"Contextual modal type theory","volume":"9","author":"Nanevski","year":"2008","journal-title":"ACM Trans. Comput. Log. (TOCL)"},{"key":"S0956796815000118_ref32","doi-asserted-by":"crossref","unstructured":"Nanevski A. (2002) Meta-programming with names and necessity. In International Conference on Functional Programming (ICFP). New York: ACM.","DOI":"10.1145\/581478.581498"},{"key":"S0956796815000118_ref36","doi-asserted-by":"crossref","unstructured":"Nanevski A. , Vafeiadis V. & Berdine J. (2010) Structuring the verification of heap-manipulating programs. In ACM Symposium on Principles of Programming Languages (POPL). New York: ACM.","DOI":"10.1145\/1706299.1706331"},{"key":"S0956796815000118_ref20","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"S0956796815000118_ref1","unstructured":"Allen S. F. , Constable R. L. , Howe D. J. & Aitken W. E. (1990) The semantics of reflected proof. In IEEE Symposium on Logic in Computer Science (LICS). New York: IEEE."},{"key":"S0956796815000118_ref44","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487248"},{"key":"S0956796815000118_ref50","doi-asserted-by":"crossref","unstructured":"Vafeiadis V. (2013) Adjustable references. In International Conference on Interactive Theorem Proving (ITP). Berlin: Springer.","DOI":"10.1007\/978-3-642-39634-2_24"},{"key":"S0956796815000118_ref15","first-page":"1382","article-title":"Formal proof\u2013-the four-color theorem","volume":"55","author":"Gonthier","year":"2008","journal-title":"Not. AMS"},{"key":"S0956796815000118_ref11","doi-asserted-by":"crossref","unstructured":"Chlipala A. (2011b) Mostly-automated verification of low-level programs in computational separation logic. In ACM Conference on Programming Languages Design and Implementation (PLDI), pp. 234\u2013245. New York: ACM.","DOI":"10.1145\/1993316.1993526"},{"key":"S0956796815000118_ref49","unstructured":"The Coq Development Team. (2012) The Coq Proof Assistant Reference Manual\u2013Version V8.4."},{"key":"S0956796815000118_ref17","unstructured":"Gonthier G. , Mahboubi A. & Tassi E. (2008) A Small Scale Reflection Extension for the Coq System. Technical Report, INRIA."},{"key":"S0956796815000118_ref29","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90069-X"},{"key":"S0956796815000118_ref41","unstructured":"Sacerdoti Coen C. (2004) Mathematical Knowledge Management and Interactive Theorem Proving. PhD Thesis, University of Bologna."},{"key":"S0956796815000118_ref39","doi-asserted-by":"crossref","unstructured":"Pollack R. (1995) On extensibility of proof checkers. In TYPES. Berlin: Springer.","DOI":"10.1007\/3-540-60579-7_8"},{"key":"S0956796815000118_ref22","first-page":"227","volume-title":"Proof Theory","author":"Howe","year":"1992"},{"key":"S0956796815000118_ref14","doi-asserted-by":"crossref","unstructured":"Devriese D. & Piessens F. (2013) Typed syntactic meta-programming. In International Conference on Functional Programming (ICFP). New York: ACM.","DOI":"10.1145\/2500365.2500575"},{"key":"S0956796815000118_ref21","unstructured":"Harrison J. (1995) Metatheory and Reflection in Theorem Proving: A Survey and Critique. Technical Report CRC-053. SRI Cambridge, Millers Yard, Cambridge, UK."},{"key":"S0956796815000118_ref2","doi-asserted-by":"crossref","unstructured":"Armand M. , Gr\u00e9goire B. , Spiwack A. & Th\u00e9ry L. (2010) Extending Coq with imperative features and its application to SAT verification. In International Conference on Interactive Theorem Proving (ITP). Berlin: Springer.","DOI":"10.1007\/978-3-642-14052-5_8"},{"key":"S0956796815000118_ref46","doi-asserted-by":"crossref","unstructured":"Sozeau M. & Oury N. (2008) First-class type classes. In International Conference on Theorem Proving in Higher Order Logics (TPHOLs). Berlin: Springer.","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"S0956796815000118_ref30","doi-asserted-by":"crossref","unstructured":"Miculan M. & Paviotti M. (2012) Synthesis of distributed mobile programs using monadic types in coq. In International Conference on Interactive Theorem Proving (ITP). Berlin: Springer.","DOI":"10.1007\/978-3-642-32347-8_13"},{"key":"S0956796815000118_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-77572-7_6"},{"key":"S0956796815000118_ref18","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796813000051"},{"key":"S0956796815000118_ref40","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.12.120"},{"key":"S0956796815000118_ref51","doi-asserted-by":"crossref","unstructured":"van der Walt P. & Swierstra W. (2013) Engineering proof by reflection in Agda. In Implementation and Application of Functional Languages (IFL).","DOI":"10.1007\/978-3-642-41582-1_10"},{"key":"S0956796815000118_ref43","doi-asserted-by":"crossref","unstructured":"Sch\u00fcrmann C. , Poswolsky A. & Sarnat J. (2005) The \u2207-calculus. Functional programming with higher-order encodings. In International Conference on Typed Lambda Calculi and Applications (TLCA). Berlin: Springer.","DOI":"10.1007\/11417170_25"},{"key":"S0956796815000118_ref38","doi-asserted-by":"crossref","unstructured":"Pientka B. & Dunfield J. (2008) Programming with proofs and explicit contexts. In International Symposium on Principles and Practice of Declarative Programming (PPDP). New York: ACM.","DOI":"10.1145\/1389449.1389469"},{"key":"S0956796815000118_ref37","doi-asserted-by":"crossref","unstructured":"Pientka B. (2008) A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In ACM Symposium on Principles of Programming Languages (POPL). New York: ACM.","DOI":"10.1145\/1328438.1328483"},{"key":"S0956796815000118_ref6","doi-asserted-by":"publisher","DOI":"10.1016\/B978-044450813-3\/50020-5"},{"key":"S0956796815000118_ref12","doi-asserted-by":"crossref","unstructured":"Claret G. , del Carmen Gonz\u00e1lez Huesca L. , R\u00e9gis-Gianas Y. & Ziliani B. (2013) Lightweight proof by reflection using a posteriori simulation of effectful computation. In International Conference on Interactive Theorem Proving (ITP). Berlin: Springer.","DOI":"10.1007\/978-3-642-39634-2_8"},{"key":"S0956796815000118_ref34","doi-asserted-by":"crossref","unstructured":"Nanevski A. , Morrisett G. , Shinnar A. , Govereau, P. & Birkedal L. (2008c) Ynot: Dependent types for imperative programs. In International Conference on Functional Programming (ICFP). New York: ACM.","DOI":"10.1145\/1411204.1411237"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796815000118","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T02:29:45Z","timestamp":1559874585000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796815000118\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"references-count":52,"alternative-id":["S0956796815000118"],"URL":"https:\/\/doi.org\/10.1017\/s0956796815000118","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]},"article-number":"e12"}}