{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:05:47Z","timestamp":1779836747020,"version":"3.53.1"},"reference-count":31,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2013,10,29]],"date-time":"2013-10-29T00:00:00Z","timestamp":1383004800000},"content-version":"unspecified","delay-in-days":120,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2013,7]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Most interactive theorem provers provide support for some form of user-customizable proof automation. In a number of popular systems, such as Coq and Isabelle, this automation is achieved primarily through\n                    <jats:italic>tactics<\/jats:italic>\n                    , which are programmed in a separate language from that of the prover's base logic. While tactics are clearly useful in practice, they can be difficult to maintain and compose because, unlike lemmas, their behavior cannot be specified within the expressive type system of the prover itself.\n                  <\/jats:p>\n                  <jats:p>\n                    We propose a novel approach to proof automation in Coq that allows the user to specify the behavior of custom automated routines in terms of Coq's own type system. Our approach involves a sophisticated application of Coq's\n                    <jats:italic>canonical structures<\/jats:italic>\n                    , which generalize Haskell type classes and facilitate a flexible style of dependently-typed logic programming. Specifically, just as Haskell type classes are used to infer the canonical implementation of an overloaded term at a given type, canonical structures can be used to infer the canonical\n                    <jats:italic>proof<\/jats:italic>\n                    of an overloaded\n                    <jats:italic>lemma<\/jats:italic>\n                    for a given instantiation of its parameters. We present a series of design patterns for canonical structure programming that enable one to carefully and predictably coax Coq's type inference engine into triggering the execution of user-supplied algorithms during unification, and we illustrate these patterns through several realistic examples drawn from Hoare Type Theory. We assume no prior knowledge of Coq and describe the relevant aspects of Coq type inference from first principles.\n                  <\/jats:p>","DOI":"10.1017\/s0956796813000051","type":"journal-article","created":{"date-parts":[[2013,10,29]],"date-time":"2013-10-29T10:36:59Z","timestamp":1383043019000},"page":"357-401","source":"Crossref","is-referenced-by-count":14,"title":["How to make ad hoc proof automation less ad hoc"],"prefix":"10.1017","volume":"23","author":[{"given":"GEORGES","family":"GONTHIER","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"BETA","family":"ZILIANI","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"ALEKSANDAR","family":"NANEVSKI","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"DEREK","family":"DREYER","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2013,10,29]]},"reference":[{"key":"S0956796813000051_ref28","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1145\/1863543.1863591","volume-title":"Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming","author":"Stampoulis","year":"2010"},{"key":"S0956796813000051_ref22","first-page":"163","volume-title":"ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming","author":"Pientka","year":"2008"},{"key":"S0956796813000051_ref30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15205-4_40"},{"key":"S0956796813000051_ref5","first-page":"241","volume-title":"ACM SIGPLAN International Conference on Functional Programming","author":"Chakravarty","year":"2005"},{"key":"S0956796813000051_ref27","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000119"},{"key":"S0956796813000051_ref20","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1145\/1863543.1863596","volume-title":"Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming","author":"Morris","year":"2010"},{"key":"S0956796813000051_ref25","doi-asserted-by":"crossref","first-page":"292","DOI":"10.1145\/263699.263742","volume-title":"Proceedings of the 24th ACM SIGPLAN\u2013SIGACT Symposium on Principles of Programming Languages","author":"Sa\u00efbi","year":"1997"},{"key":"S0956796813000051_ref24","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"S0956796813000051_ref18","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"S0956796813000051_ref23","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.12.120"},{"key":"S0956796813000051_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22863-6_10"},{"key":"S0956796813000051_ref9","first-page":"1382","article-title":"Formal proof \u2013 the four-color theorem","volume":"55","author":"Gonthier","year":"2008","journal-title":"Not. AMS"},{"key":"S0956796813000051_ref19","first-page":"255","volume-title":"International Conference on Logic Programming","author":"Miller","year":"1991"},{"key":"S0956796813000051_ref2","first-page":"143","volume-title":"Twenty-Sixth Annual IEEE Symposium on Logic in Computer Science","author":"Barras","year":"2011"},{"key":"S0956796813000051_ref3","first-page":"86","volume-title":"TPHOLs","author":"Bertot","year":"2008"},{"key":"S0956796813000051_ref31","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1145\/75277.75283","volume-title":"Proceedings of the 16th Annual ACM SIGPLAN\u2013SIGACT Symposium on Principles of Programming Languages","author":"Wadler","year":"1989"},{"key":"S0956796813000051_ref6","unstructured":"Chlipala A. (2008) Certified Programming with Dependent Types. Available at: http:\/\/adam.hlipala.net\/cpdt."},{"key":"S0956796813000051_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"S0956796813000051_ref11","first-page":"95","article-title":"An introduction to small scale reflection in Coq","volume":"3","author":"Gonthier","year":"2010","journal-title":"J. Formalized Reason."},{"key":"S0956796813000051_ref17","doi-asserted-by":"publisher","DOI":"10.1145\/1743546.1743574"},{"key":"S0956796813000051_ref21","first-page":"261","volume-title":"Proceedings of the 37th annual ACM SIGPLAN\u2013SIGACT Symposium on Principles of Programming Languages","author":"Nanevski","year":"2010"},{"key":"S0956796813000051_ref12","doi-asserted-by":"crossref","unstructured":"Gonthier G. , Ziliani B. , Nanevski A. & Dreyer D. (2012) How to make ad hoc proof automation less ad hoc. Supporting material available at: http:\/\/www.mpi-sws.org\/~beta\/lessadhoc.","DOI":"10.1145\/2034773.2034798"},{"key":"S0956796813000051_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(81)90040-2"},{"key":"S0956796813000051_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_7"},{"key":"S0956796813000051_ref15","first-page":"275","volume-title":"Proceedings of the ACM SIGPLAN\u2013SIGACT Symposium on Principles of Programming Languages","author":"Jia","year":"2010"},{"key":"S0956796813000051_ref29","first-page":"273","volume-title":"39th ACM Symposium on Principles of Programming Languages","author":"Stampoulis","year":"2012"},{"key":"S0956796813000051_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_8"},{"key":"S0956796813000051_ref14","doi-asserted-by":"publisher","DOI":"10.1145\/227699.227700"},{"key":"S0956796813000051_ref4","unstructured":"Braibant T. & Pous D. (2010) Rewriting modulo associativity and commutativity in Coq. Second Coq Workshop."},{"key":"S0956796813000051_ref16","first-page":"230","volume-title":"Proceedings of the European Symposium on Programming","author":"Jones","year":"2000"},{"key":"S0956796813000051_ref7","first-page":"234","volume-title":"Proceedings of the ACM SIGPLAN 2011 Conference on Programming Language Design and Implementation","author":"Chlipala","year":"2011"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796813000051","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:36:30Z","timestamp":1779834990000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796813000051\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,7]]},"references-count":31,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2013,7]]}},"alternative-id":["S0956796813000051"],"URL":"https:\/\/doi.org\/10.1017\/s0956796813000051","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,7]]}}}