{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T07:43:49Z","timestamp":1770277429306,"version":"3.49.0"},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2018,7,30]],"date-time":"2018-07-30T00:00:00Z","timestamp":1532908800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,7,30]]},"abstract":"<jats:p>\n            Coq supports a range of built-in tactics, which are engineered primarily to support\n            <jats:italic>backward reasoning<\/jats:italic>\n            . Starting from a desired goal, the Coq programmer can use these tactics to manipulate the proof state interactively, applying axioms or lemmas to break the goal into subgoals until all subgoals have been solved. Additionally, it provides support for\n            <jats:italic>tactic programming<\/jats:italic>\n            via OCaml and Ltac, so that users can roll their own custom proof automation routines.\n          <\/jats:p>\n          <jats:p>\n            Unfortunately, though, these tactic languages share a significant weakness. They do not offer the tactic programmer any static guarantees about the soundness of their custom tactics, making large tactic developments difficult to maintain. To address this limitation, Ziliani et al. previously proposed\n            <jats:bold>Mtac<\/jats:bold>\n            , a new typed approach to custom proof automation in Coq which provides the static guarantees that OCaml and Ltac are missing. However, despite its name, Mtac is really more of a metaprogramming language than it is a full-blown tactic language: it misses an essential feature of tactic programming, namely the ability to directly manipulate Coq\u2019s proof state and perform backward reasoning on it.\n          <\/jats:p>\n          <jats:p>\n            In this paper, we present\n            <jats:bold>Mtac2<\/jats:bold>\n            , a next-generation version of Mtac that combines its support for typed metaprogramming with additional support for the programming of backward-reasoning tactics in the style of Ltac. In so doing, Mtac2 introduces a novel feature in tactic programming languages\u2014what we call\n            <jats:italic>typed backward reasoning<\/jats:italic>\n            . With this feature, Mtac2 is capable of statically ruling out several classes of errors that would otherwise remain undetected at tactic definition time. We demonstrate the utility of Mtac2\u2019s typed tactics by porting several tactics from a large Coq development, the Iris Proof Mode, from Ltac to Mtac2.\n          <\/jats:p>","DOI":"10.1145\/3236773","type":"journal-article","created":{"date-parts":[[2018,7,31]],"date-time":"2018-07-31T19:41:18Z","timestamp":1533066078000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Mtac2: typed tactics for backward reasoning in Coq"],"prefix":"10.1145","volume":"2","author":[{"given":"Jan-Oliver","family":"Kaiser","sequence":"first","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Beta","family":"Ziliani","sequence":"additional","affiliation":[{"name":"Universidad Nacional de C\u00f3rdoba, Argentina \/ CONICET, Argentina"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robbert","family":"Krebbers","sequence":"additional","affiliation":[{"name":"Delft University of Technology, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yann","family":"R\u00e9gis-Gianas","sequence":"additional","affiliation":[{"name":"IRIF, France \/ CNRS, France \/ University of Paris Diderot, France \/ Inria, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Derek","family":"Dreyer","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2018,7,30]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Retrieved","author":"Development Team The Agda","year":"2018","unstructured":"The Agda Development Team . 2018 . Reflection . Retrieved March 16, 2018 from https:\/\/agda.readthedocs.io\/en\/v2.5.3\/ language\/reflection.html The Agda Development Team. 2018. Reflection. Retrieved March 16, 2018 from https:\/\/agda.readthedocs.io\/en\/v2.5.3\/ language\/reflection.html"},{"key":"e_1_2_2_2_1","volume-title":"Claudio Sacerdoti Coen, and Enrico Tassi","author":"Asperti Andrea","year":"2009","unstructured":"Andrea Asperti , Wilmer Ricciotti , Claudio Sacerdoti Coen, and Enrico Tassi . 2009 . A new type for tactics. PLMMS ( 2009), 22. Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, and Enrico Tassi. 2009. A new type for tactics. PLMMS (2009), 22."},{"key":"e_1_2_2_3_1","volume-title":"Dedukti: A universal proof checker. In Journ\u00e9es communes LTP - LAC. https:\/\/hal-mines-paristech.archives-ouvertes.fr\/hal-01537578","author":"Boespflug Mathieu","year":"2012","unstructured":"Mathieu Boespflug , Quentin Carbonneaux , Olivier Hermant , and Ronan Saillard . 2012 . Dedukti: A universal proof checker. In Journ\u00e9es communes LTP - LAC. https:\/\/hal-mines-paristech.archives-ouvertes.fr\/hal-01537578 Mathieu Boespflug, Quentin Carbonneaux, Olivier Hermant, and Ronan Saillard. 2012. Dedukti: A universal proof checker. In Journ\u00e9es communes LTP - LAC. https:\/\/hal-mines-paristech.archives-ouvertes.fr\/hal-01537578"},{"key":"e_1_2_2_4_1","doi-asserted-by":"crossref","unstructured":"Rapha\u00ebl Cauderlier. 2018. Tactics and certificates in Meta Dedukti. In ITP (ITP \u201818).  Rapha\u00ebl Cauderlier. 2018. Tactics and certificates in Meta Dedukti. In ITP (ITP \u201818).","DOI":"10.1007\/978-3-319-94821-8_9"},{"key":"e_1_2_2_5_1","unstructured":"Rapha\u00ebl Cauderlier and Fran\u00e7ois Thir\u00e9. {n. d.}. Meta Dedukti. http:\/\/deducteam.gforge.inria.fr\/metadedukti\/  Rapha\u00ebl Cauderlier and Fran\u00e7ois Thir\u00e9. {n. d.}. Meta Dedukti. http:\/\/deducteam.gforge.inria.fr\/metadedukti\/"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951932"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_8"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110278"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90014-7"},{"key":"e_1_2_2_10_1","article-title":"Tactics for mechanized reasoning: a commentary on Milner (1984) \u2018The use of machines to assist in rigorous proof","volume":"373","author":"Gordon M. J. C.","year":"2015","unstructured":"M. J. C. Gordon . 2015 . Tactics for mechanized reasoning: a commentary on Milner (1984) \u2018The use of machines to assist in rigorous proof \u2019. Philosophical Transactions of the Royal Society of London A: Mathematical, Physical and Engineering Sciences 373 , 2039 (2015). M. J. C. Gordon. 2015. Tactics for mechanized reasoning: a commentary on Milner (1984) \u2018The use of machines to assist in rigorous proof\u2019. Philosophical Transactions of the Royal Society of London A: Mathematical, Physical and Engineering Sciences 373, 2039 (2015).","journal-title":"Philosophical Transactions of the Royal Society of London A: Mathematical, Physical and Engineering Sciences"},{"key":"e_1_2_2_11_1","volume-title":"Wadsworth","author":"Gordon Michael J. C.","year":"1979","unstructured":"Michael J. C. Gordon , Robin Milner , and Christopher P . Wadsworth . 1979 . Edinburgh LCF. LNCS , Vol . 78. Michael J. C. Gordon, Robin Milner, and Christopher P. Wadsworth. 1979. Edinburgh LCF. LNCS, Vol. 78."},{"key":"e_1_2_2_12_1","doi-asserted-by":"crossref","unstructured":"Jason Gross Andres Erbsen and Adam Chlipala. 2018. Reification by Parametricity: Fast Setup for Proof by Reflection in Two Lines of Ltac. In ITP (ITP \u201818).  Jason Gross Andres Erbsen and Adam Chlipala. 2018. Reification by Parametricity: Fast Setup for Proof by Reflection in Two Lines of Ltac. In ITP (ITP \u201818).","DOI":"10.1007\/978-3-319-94821-8_17"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_2_2_14_1","volume-title":"Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Submitted for publication","author":"Jung Ralf","year":"2017","unstructured":"Ralf Jung , Robbert Krebbers , Jacques-Henri Jourdan , Ale\u0161 Bizjak , Lars Birkedal , and Derek Dreyer . 2017. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Submitted for publication ( 2017 ). Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ale\u0161 Bizjak, Lars Birkedal, and Derek Dreyer. 2017. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. Submitted for publication (2017)."},{"key":"e_1_2_2_15_1","first-page":"1","article-title":"Strong logic for weak memory: Reasoning about release-acquire consistency in Iris","volume":"74","author":"Kaiser Jan-Oliver","year":"2017","unstructured":"Jan-Oliver Kaiser , Hoang-Hai Dang , Derek Dreyer , Ori Lahav , and Viktor Vafeiadis . 2017 . Strong logic for weak memory: Reasoning about release-acquire consistency in Iris . In ECOOP (LIPIcs) , Vol. 74. 17: 1 \u2013 17 :29. Jan-Oliver Kaiser, Hoang-Hai Dang, Derek Dreyer, Ori Lahav, and Viktor Vafeiadis. 2017. Strong logic for weak memory: Reasoning about release-acquire consistency in Iris. In ECOOP (LIPIcs), Vol. 74. 17:1\u201317:29.","journal-title":"ECOOP (LIPIcs)"},{"key":"e_1_2_2_16_1","doi-asserted-by":"crossref","unstructured":"Jan-Oliver Kaiser Beta Ziliani Robbert Krebbers Yann R\u00e9gis-Gianas and Derek Dreyer. 2018. Coq repository for Mtac2. https:\/\/github.com\/Mtac2\/Mtac2\/ .  Jan-Oliver Kaiser Beta Ziliani Robbert Krebbers Yann R\u00e9gis-Gianas and Derek Dreyer. 2018. Coq repository for Mtac2. https:\/\/github.com\/Mtac2\/Mtac2\/ .","DOI":"10.1145\/3236773"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_2_18_1","volume-title":"Retrieved","author":"Malecha Gregory","year":"2018","unstructured":"Gregory Malecha , Abhishek Anand , Simon Boulier , and Matthieu Sozeau . 2018 . Reflection library for Coq . Retrieved March 16, 2018 from https:\/\/github.com\/Template-Coq\/template-coq Gregory Malecha, Abhishek Anand, Simon Boulier, and Matthieu Sozeau. 2018. Reflection library for Coq. Retrieved March 16, 2018 from https:\/\/github.com\/Template-Coq\/template-coq"},{"key":"e_1_2_2_19_1","first-page":"532","article-title":"Extensible and efficient automation through reflective tactics","volume":"9632","author":"Malecha Gregory","year":"2016","unstructured":"Gregory Malecha and Jesper Bengtson . 2016 . Extensible and efficient automation through reflective tactics . In ESOP (LNCS) , Vol. 9632. 532 \u2013 559 . Gregory Malecha and Jesper Bengtson. 2016. Extensible and efficient automation through reflective tactics. In ESOP (LNCS), Vol. 9632. 532\u2013559.","journal-title":"ESOP (LNCS)"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006326"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"e_1_2_2_22_1","volume-title":"Retrieved","author":"P\u00e9drot Pierre-Marie","year":"2016","unstructured":"Pierre-Marie P\u00e9drot . 2016 . The Coq tactic engine . Retrieved March 16, 2018 from http:\/\/coqhott.gforge.inria.fr\/blog\/ coq-tactic-engine\/ Pierre-Marie P\u00e9drot. 2016. The Coq tactic engine. Retrieved March 16, 2018 from http:\/\/coqhott.gforge.inria.fr\/blog\/ coq-tactic-engine\/"},{"key":"e_1_2_2_23_1","volume-title":"Retrieved","author":"P\u00e9drot Pierre-Marie","year":"2018","unstructured":"Pierre-Marie P\u00e9drot . 2018 . A standalone implementation of Ltac2 as a Coq plugin . Retrieved March 16, 2018 from https:\/\/github.com\/ppedrot\/ltac2\/ Pierre-Marie P\u00e9drot. 2018. A standalone implementation of Ltac2 as a Coq plugin. Retrieved March 16, 2018 from https:\/\/github.com\/ppedrot\/ltac2\/"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328483"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"e_1_2_2_26_1","first-page":"499","article-title":"Universe Polymorphism in Coq","volume":"8558","author":"Sozeau Matthieu","year":"2014","unstructured":"Matthieu Sozeau and Nicolas Tabareau . 2014 . Universe Polymorphism in Coq . In ITP (LNCS) , Vol. 8558. 499 \u2013 514 . Matthieu Sozeau and Nicolas Tabareau. 2014. Universe Polymorphism in Coq. In ITP (LNCS), Vol. 8558. 499\u2013514.","journal-title":"ITP (LNCS)"},{"key":"e_1_2_2_27_1","unstructured":"Arnaud Spiwack. 2010. An abstract type for constructing tactics in Coq. In Proof Search in Type Theory.  Arnaud Spiwack. 2010. An abstract type for constructing tactics in Coq. In Proof Search in Type Theory."},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863591"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133913"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158152"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500579"},{"key":"e_1_2_2_32_1","volume-title":"Mtac: A monad for typed tactic programming in Coq. JFP 25","author":"Ziliani Beta","year":"2015","unstructured":"Beta Ziliani , Derek Dreyer , Neelakantan R. Krishnaswami , Aleksandar Nanevski , and Viktor Vafeiadis . 2015 . Mtac: A monad for typed tactic programming in Coq. JFP 25 (2015). Beta Ziliani, Derek Dreyer, Neelakantan R. Krishnaswami, Aleksandar Nanevski, and Viktor Vafeiadis. 2015. Mtac: A monad for typed tactic programming in Coq. JFP 25 (2015)."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3236773","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3236773","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T21:41:28Z","timestamp":1750282888000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3236773"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7,30]]},"references-count":32,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2018,7,30]]}},"alternative-id":["10.1145\/3236773"],"URL":"https:\/\/doi.org\/10.1145\/3236773","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,7,30]]},"assertion":[{"value":"2018-07-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}