{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:47:28Z","timestamp":1772164048512,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":31,"publisher":"ACM","license":[{"start":{"date-parts":[[2013,9,25]],"date-time":"2013-09-25T00:00:00Z","timestamp":1380067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2013,9,25]]},"DOI":"10.1145\/2500365.2500579","type":"proceedings-article","created":{"date-parts":[[2013,9,25]],"date-time":"2013-09-25T09:13:17Z","timestamp":1380100397000},"page":"87-100","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":22,"title":["Mtac"],"prefix":"10.1145","author":[{"given":"Beta","family":"Ziliani","sequence":"first","affiliation":[{"name":"MPI-SWS, Saarbruecken, Germany"}]},{"given":"Derek","family":"Dreyer","sequence":"additional","affiliation":[{"name":"MPI-SWS, Saarbruecken, Germany"}]},{"given":"Neelakantan R.","family":"Krishnaswami","sequence":"additional","affiliation":[{"name":"MPI-SWS, Saarbruecken, Germany"}]},{"given":"Aleksandar","family":"Nanevski","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Madrid, Spain"}]},{"given":"Viktor","family":"Vafeiadis","sequence":"additional","affiliation":[{"name":"MPI-SWS, Kaiserslautern, Germany"}]}],"member":"320","published-online":{"date-parts":[[2013,9,25]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/778522.778527"},{"key":"e_1_3_2_1_2_1","volume-title":"Interactive theorem proving and program development : Coq'Art : the calculus of inductive constructions. Texts in theoretical computer science","author":"Bertot Y.","year":"2004","unstructured":"Y. Bertot , P. Cast\u00e9ran , G. Huet , and C. Paulin-Mohring . Interactive theorem proving and program development : Coq'Art : the calculus of inductive constructions. Texts in theoretical computer science . Springer , 2004 . Y. Bertot, P. Cast\u00e9ran, G. Huet, and C. Paulin-Mohring. Interactive theorem proving and program development : Coq'Art : the calculus of inductive constructions. Texts in theoretical computer science. Springer, 2004."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/645869.668533"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103705"},{"key":"e_1_3_2_1_5_1","unstructured":"A. Chlipala. Certified programming with dependent types. http:\/\/adam.chlipala.net\/cpdt 2008.  A. Chlipala. Certified programming with dependent types. http:\/\/adam.chlipala.net\/cpdt 2008."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993526"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_8"},{"issue":"11","key":"e_1_3_2_1_8_1","first-page":"1382","article-title":"Formal proof -- the four-color theorem","volume":"55","author":"Gonthier G.","year":"2008","unstructured":"G. Gonthier . Formal proof -- the four-color theorem . Notices of the AMS , 55 ( 11 ): 1382 -- 1393 , 2008 . G. Gonthier. Formal proof -- the four-color theorem. Notices of the AMS, 55(11):1382--93, 2008.","journal-title":"Notices of the AMS"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_14"},{"key":"e_1_3_2_1_10_1","volume-title":"INRIA","author":"Gonthier G.","year":"2008","unstructured":"G. Gonthier , A. Mahboubi , and E. Tassi . A small scale reflection extension for the Coq system. Technical report , INRIA , 2008 . G. Gonthier, A. Mahboubi, and E. Tassi. A small scale reflection extension for the Coq system. Technical report, INRIA, 2008."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034798"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581501"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429093"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1743546.1743574"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90069-X"},{"key":"e_1_3_2_1_18_1","volume-title":"ICLP 1991","author":"Miller D.","year":"1991","unstructured":"D. Miller . Unification of simply typed lamda-terms as logic programming . In ICLP 1991 . MIT Press , 1991 . D. Miller. Unification of simply typed lamda-terms as logic programming. In ICLP 1991. MIT Press, 1991."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581498"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328483"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1389449.1389469"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.12.120"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263742"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/11417170_25"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/1789277.1789293"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_23"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863591"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103690"},{"key":"e_1_3_2_1_31_1","volume-title":"The Coq Proof Assistant Reference Manual -- Version V8.4","author":"Development Team The Coq","year":"2012","unstructured":"The Coq Development Team . The Coq Proof Assistant Reference Manual -- Version V8.4 , 2012 . The Coq Development Team. The Coq Proof Assistant Reference Manual -- Version V8.4, 2012."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2487241.2487248"}],"event":{"name":"ICFP'13: ACM SIGPLAN International Conference on Functional Programming","location":"Boston Massachusetts USA","acronym":"ICFP'13","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","Northeastern University"]},"container-title":["Proceedings of the 18th ACM SIGPLAN international conference on Functional programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2500365.2500579","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2500365.2500579","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:34:32Z","timestamp":1750217672000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2500365.2500579"}},"subtitle":["a monad for typed tactic programming in Coq"],"short-title":[],"issued":{"date-parts":[[2013,9,25]]},"references-count":31,"alternative-id":["10.1145\/2500365.2500579","10.1145\/2500365"],"URL":"https:\/\/doi.org\/10.1145\/2500365.2500579","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2544174.2500579","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2013,9,25]]},"assertion":[{"value":"2013-09-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}