{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:48:47Z","timestamp":1750308527932,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":16,"publisher":"ACM","license":[{"start":{"date-parts":[[2014,7,17]],"date-time":"2014-07-17T00:00:00Z","timestamp":1405555200000},"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":[[2014,7,17]]},"DOI":"10.1145\/2631172.2631181","type":"proceedings-article","created":{"date-parts":[[2014,7,11]],"date-time":"2014-07-11T12:10:42Z","timestamp":1405080642000},"page":"1-8","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Automatically Deriving Schematic Theorems for Dynamic Contexts"],"prefix":"10.1145","author":[{"given":"Olivier Savary","family":"B\u00e9langer","sequence":"first","affiliation":[{"name":"McGill University, Canada"}]},{"given":"Kaustuv","family":"Chaudhuri","sequence":"additional","affiliation":[{"name":"INRIA, France"}]}],"member":"320","published-online":{"date-parts":[[2014,7,17]]},"reference":[{"key":"e_1_3_2_1_1_1","first-page":"85","volume-title":"LPAR","author":"Delahaye D.","year":"1955","unstructured":"D. Delahaye . A tactic language for the system Coq . In LPAR , pages 85 -- 95 . Springer LNCS 1955 , 2000. D. Delahaye. A tactic language for the system Coq. In LPAR, pages 85--95. Springer LNCS 1955, 2000."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9194-x"},{"key":"e_1_3_2_1_3_1","volume-title":"The next 700 challenge problems for reasoning with higher-order abstract syntax representations: Part 1---A foundational view","author":"Felty A. P.","year":"2014","unstructured":"A. P. Felty , A. Momigliano , and B. Pientka . The next 700 challenge problems for reasoning with higher-order abstract syntax representations: Part 1---A foundational view , 2014 . A. P. Felty, A. Momigliano, and B. Pientka. The next 700 challenge problems for reasoning with higher-order abstract syntax representations: Part 1---A foundational view, 2014."},{"key":"e_1_3_2_1_4_1","volume-title":"The next 700 challenge problems for reasoning with higher-order abstract syntax representations: Part 2---A survey","author":"Felty A. P.","year":"2014","unstructured":"A. P. Felty , A. Momigliano , and B. Pientka . The next 700 challenge problems for reasoning with higher-order abstract syntax representations: Part 2---A survey , 2014 . A. P. Felty, A. Momigliano, and B. Pientka. The next 700 challenge problems for reasoning with higher-order abstract syntax representations: Part 2---A survey, 2014."},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71070-7_13"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2010.09.004"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9218-1"},{"key":"e_1_3_2_1_9_1","volume-title":"Tenth Symposium of the Mathematical Foundations of Computer Science, IBM Japan","author":"Miller D.","year":"1985","unstructured":"D. Miller and G. Nadathur . A computational logic approach to syntax and semantics . Presented at the Tenth Symposium of the Mathematical Foundations of Computer Science, IBM Japan , May 1985 . D. Miller and G. Nadathur. A computational logic approach to syntax and semantics. Presented at the Tenth Symposium of the Mathematical Foundations of Computer Science, IBM Japan, May 1985."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/2331097"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/788023.789055"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/53990.54010"},{"key":"e_1_3_2_1_14_1","volume-title":"Twelf User's Guide","author":"Pfenning F.","year":"2002","unstructured":"F. Pfenning and C. Schuermann . Twelf User's Guide . Carnegie Mellon University , 1.4 edition, 2002 . F. Pfenning and C. Schuermann. Twelf User's Guide. Carnegie Mellon University, 1.4 edition, 2002."},{"key":"e_1_3_2_1_15_1","first-page":"202","volume-title":"System description: Twelf --- A meta-logical framework for deductive systems","author":"Pfenning F.","year":"1999","unstructured":"F. Pfenning and C. Sch\u00fcrmann . System description: Twelf --- A meta-logical framework for deductive systems . In H. Ganzinger, editor, CADE, pages 202 -- 206 . Springer LNAI 1632, 1999 . F. Pfenning and C. Sch\u00fcrmann. System description: Twelf --- A meta-logical framework for deductive systems. In H. Ganzinger, editor, CADE, pages 202--206. Springer LNAI 1632, 1999."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_2"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2505879.2505889"}],"event":{"name":"LFMTP '14: Theory and Practice","acronym":"LFMTP '14","location":"Vienna Austria"},"container-title":["Proceedings of the 2014 International Workshop on Logical Frameworks and Meta-languages: Theory and Practice"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2631172.2631181","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2631172.2631181","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T18:55:48Z","timestamp":1750272948000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2631172.2631181"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,7,17]]},"references-count":16,"alternative-id":["10.1145\/2631172.2631181","10.1145\/2631172"],"URL":"https:\/\/doi.org\/10.1145\/2631172.2631181","relation":{},"subject":[],"published":{"date-parts":[[2014,7,17]]},"assertion":[{"value":"2014-07-17","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}