{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:39:24Z","timestamp":1750307964640,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":48,"publisher":"ACM","license":[{"start":{"date-parts":[[2007,7,14]],"date-time":"2007-07-14T00:00:00Z","timestamp":1184371200000},"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":[[2007,7,14]]},"DOI":"10.1145\/1273920.1273931","type":"proceedings-article","created":{"date-parts":[[2012,10,10]],"date-time":"2012-10-10T14:45:29Z","timestamp":1349880329000},"page":"75-86","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Mechanized metatheory model-checking"],"prefix":"10.1145","author":[{"given":"James","family":"Cheney","sequence":"first","affiliation":[{"name":"University of Edinburgh"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alberto","family":"Momigliano","sequence":"additional","affiliation":[{"name":"University of Edinburgh\/DSI, University of Milan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2007,7,14]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_3_2_1_1_1","DOI":"10.1145\/1044731.1044735"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_2_1","DOI":"10.1007\/11541868_4"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_3_1","DOI":"10.1016\/0743-1066(90)90023-X"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_4_1","DOI":"10.5555\/1030033.1030056"},{"key":"e_1_3_2_1_5_1","first-page":"111","volume-title":"Proc. ECAI-90","author":"Brogi A.","year":"1990","unstructured":"A. Brogi , P. Mancarella , D. Pedreschi , and F. Turini . Universal quantification by case analysis . In Proc. ECAI-90 , pages 111 -- 116 , 1990 . A. Brogi, P. Mancarella, D. Pedreschi, and F. Turini. Universal quantification by case analysis. In Proc. ECAI-90, pages 111--116, 1990."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_6_1","DOI":"10.5555\/648222.751401"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_7_1","DOI":"10.1007\/978-3-540-32033-3_7"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_8_1","DOI":"10.1145\/1086365.1086389"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_9_1","DOI":"10.1007\/978-3-540-31982-5_24"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_10_1","DOI":"10.1007\/11799573_27"},{"key":"e_1_3_2_1_11_1","volume-title":"ICLP","author":"Cheney J.","year":"2004","unstructured":"J. Cheney and C. Urban . Alpha-Prolog: A logic programming language with names, binding and alpha-equivalence . In ICLP 2004 , number 3132 in LNCS, pages 269--283, 2004. J. Cheney and C. Urban. Alpha-Prolog: A logic programming language with names, binding and alpha-equivalence. In ICLP 2004, number 3132 in LNCS, pages 269--283, 2004."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_14_1","DOI":"10.1145\/351240.351266"},{"key":"e_1_3_2_1_15_1","volume-title":"Model Checking","author":"Clarke E. M.","year":"2000","unstructured":"E. M. Clarke , O. Grumberg , and D. A. Peled . Model Checking . MIT Press , 2000 . E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 2000."},{"key":"e_1_3_2_1_16_1","volume-title":"J. -L","author":"Comon H.","year":"1991","unstructured":"H. Comon . Disunification: a survey . In J. -L . Lassez and G.Plotkin, editors, Computational Logic. MIT Press , Cambridge, MA, 1991 . H. Comon. Disunification: a survey. In J. -L. Lassez and G.Plotkin, editors, Computational Logic. MIT Press, Cambridge, MA, 1991."},{"unstructured":"M. Fairbairn. Solution to part 3 of the POPLMark Challenge. Available at the POPLMark Wiki http:\/\/fling-l.seas.upenn.edu\/~plclub\/cgi-bin\/poplmark.  M. Fairbairn. Solution to part 3 of the POPLMark Challenge. Available at the POPLMark Wiki http:\/\/fling-l.seas.upenn.edu\/~plclub\/cgi-bin\/poplmark.","key":"e_1_3_2_1_17_1"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_18_1","DOI":"10.1145\/1069774.1069779"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_19_1","DOI":"10.1016\/S0304-3975(00)00330-3"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_20_1","DOI":"10.1007\/s001650200016"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_21_1","DOI":"10.1016\/0743-1066(94)90034-5"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_22_1","DOI":"10.1016\/0743-1066(93)90007-4"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_23_1","DOI":"10.1145\/1042038.1042041"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_24_1","DOI":"10.1016\/0743-1066(87)90007-0"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_25_1","DOI":"10.5555\/33031.33036"},{"key":"e_1_3_2_1_26_1","first-page":"1006","volume-title":"Proceedings of the Fifth International Conference and Symposium on Logic Programming","author":"Mancarella P.","year":"1988","unstructured":"P. Mancarella and D. Pedreschi . An algebra of logic programs. In R. A. Kowalski and K. A. Bowen, editors , Proceedings of the Fifth International Conference and Symposium on Logic Programming , pages 1006 -- 1023 , Seatle , 1988 . ALP, IEEE, The MIT Press. P. Mancarella and D. Pedreschi. An algebra of logic programs. In R. A. Kowalski and K. A. Bowen, editors, Proceedings of the Fifth International Conference and Symposium on Logic Programming, pages 1006--1023, Seatle, 1988. ALP, IEEE, The MIT Press."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_27_1","DOI":"10.1145\/504077.504080"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"McMillan K. L.","year":"1993","unstructured":"K. L. McMillan . Symbolic Model Checking . Kluwer Academic Publishers , 1993 . K. L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_29_1","DOI":"10.1145\/1094622.1094628"},{"doi-asserted-by":"crossref","unstructured":"A.\n      Momigliano\n    .\n  Elimination of negation in a logical framework\n  . In P. Clote and H. Schwichtenberg editors CSL volume \n  1862\n   of \n  Lecture Notes in Computer Science pages \n  411\n  --\n  426\n  . \n  Springer 2000\n  .   A. Momigliano. Elimination of negation in a logical framework. In P. Clote and H. Schwichtenberg editors CSL volume 1862 of Lecture Notes in Computer Science pages 411--426. Springer 2000.","key":"e_1_3_2_1_30_1","DOI":"10.1007\/3-540-44622-2_28"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_31_1","DOI":"10.1145\/937555.937559"},{"doi-asserted-by":"crossref","unstructured":"J. J.\n      Moreno-Navarro\n     and \n      S.\n      Munoz-Hern\u00e1ndez\n  . \n  How to incorporate negation in a Prolog compiler\n  . In E. Pontelli and V. S. Costa editors PADL \n  2000 volume \n  1753\n   of \n  LNCS pages \n  124\n  --\n  140\n  . \n  Springer 2000.   J. J. Moreno-Navarro and S. Munoz-Hern\u00e1ndez. How to incorporate negation in a Prolog compiler. In E. Pontelli and V. S. Costa editors PADL 2000 volume 1753 of LNCS pages 124--140. Springer 2000.","key":"e_1_3_2_1_32_1","DOI":"10.1007\/3-540-46584-7_9"},{"doi-asserted-by":"crossref","unstructured":"S.\n      Munoz-Hern\u00e1ndez J.\n      Marino and \n      J. J.\n      Moreno-Navarro\n  . \n  Constructive intensional negation\n  . In Y. Kameyama and P. J. Stuckey editors FLOPS volume \n  2998\n   of \n  Lecture Notes in Computer Science pages \n  39\n  --\n  54\n  . \n  Springer 2004\n  .  S. Munoz-Hern\u00e1ndez J. Marino and J. J. Moreno-Navarro. Constructive intensional negation. In Y. Kameyama and P. J. Stuckey editors FLOPS volume 2998 of Lecture Notes in Computer Science pages 39--54. Springer 2004.","key":"e_1_3_2_1_33_1","DOI":"10.1007\/978-3-540-24754-8_5"},{"issue":"3","key":"e_1_3_2_1_34_1","article-title":"A declarative debugging scheme","volume":"1997","author":"Naish L.","year":"1997","unstructured":"L. Naish . A declarative debugging scheme . Journal of Functional and Logic Programming , 1997 ( 3 ), 1997 . L. Naish. A declarative debugging scheme. Journal of Functional and Logic Programming, 1997(3), 1997.","journal-title":"Journal of Functional and Logic Programming"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_35_1","DOI":"10.1007\/11853886_2"},{"key":"e_1_3_2_1_36_1","volume-title":"Handbook of Automated Reasoning","author":"Pfenning F.","year":"2000","unstructured":"F. Pfenning . Logical frameworks . In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning . Elsevier Science Publishers , 2000 . In preparation. F. Pfenning. Logical frameworks. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning. Elsevier Science Publishers, 2000. In preparation."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_37_1","DOI":"10.5555\/648235.753634"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_38_1","DOI":"10.1007\/s10817-005-6534-3"},{"key":"e_1_3_2_1_39_1","volume-title":"Types and Programming Languages","author":"Pierce B. C.","year":"2002","unstructured":"B. C. Pierce . Types and Programming Languages . MIT Press , 2002 . B. C. Pierce. Types and Programming Languages. MIT Press, 2002."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_40_1","DOI":"10.1016\/S0890-5401(03)00138-X"},{"key":"e_1_3_2_1_41_1","first-page":"273","volume-title":"Logic Program Synthesis and Transformation","author":"Puebla G.","year":"1999","unstructured":"G. Puebla , F. Bueno , and M. V. Hermenegildo . Combined static and dynamic assertion-based debugging of constraint logic programs . In Logic Program Synthesis and Transformation , pages 273 -- 292 , 1999 . G. Puebla, F. Bueno, and M. V. Hermenegildo. Combined static and dynamic assertion-based debugging of constraint logic programs. In Logic Program Synthesis and Transformation, pages 273--292, 1999."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_42_1","DOI":"10.5555\/647766.733615"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_43_1","DOI":"10.5555\/647769.733956"},{"key":"e_1_3_2_1_44_1","first-page":"333","volume-title":"Proceedings of the 4th International Workshop on Extensions of Logic Programming","author":"Schroeder-Heister P.","year":"1993","unstructured":"P. Schroeder-Heister . Definitional reflection and the completion. In R. Dyckhoff, editor , Proceedings of the 4th International Workshop on Extensions of Logic Programming , pages 333 -- 347 . Springer-Verlag LNAI 798 , 1993 . P. Schroeder-Heister. Definitional reflection and the completion. In R. Dyckhoff, editor, Proceedings of the 4th International Workshop on Extensions of Logic Programming, pages 333--347. Springer-Verlag LNAI 798, 1993."},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_45_1","DOI":"10.1109\/LICS.1993.287585"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_46_1","DOI":"10.1006\/inco.1995.1048"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_47_1","DOI":"10.1007\/11539452_7"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_48_1","DOI":"10.1007\/978-3-540-32033-3_7"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_49_1","DOI":"10.1016\/j.tcs.2004.06.016"},{"doi-asserted-by":"publisher","key":"e_1_3_2_1_50_1","DOI":"10.1145\/1159803.1159809"}],"event":{"sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery"],"acronym":"PPDP07","name":"PPDP07: Principles and Practice of Declarative Programming","location":"Wroclaw Poland"},"container-title":["Proceedings of the 9th ACM SIGPLAN international conference on Principles and practice of declarative programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1273920.1273931","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1273920.1273931","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T14:58:09Z","timestamp":1750258689000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1273920.1273931"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,7,14]]},"references-count":48,"alternative-id":["10.1145\/1273920.1273931","10.1145\/1273920"],"URL":"https:\/\/doi.org\/10.1145\/1273920.1273931","relation":{},"subject":[],"published":{"date-parts":[[2007,7,14]]},"assertion":[{"value":"2007-07-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}