{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:21:03Z","timestamp":1776316863547,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":45,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,9,20]],"date-time":"2022-09-20T00:00:00Z","timestamp":1663632000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["682315"],"award-info":[{"award-number":["682315"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000288","name":"Royal Society","doi-asserted-by":"publisher","award":["IES\\R2\\212106"],"award-info":[{"award-number":["IES\\R2\\212106"]}],"id":[{"id":"10.13039\/501100000288","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,9,20]]},"DOI":"10.1145\/3551357.3551375","type":"proceedings-article","created":{"date-parts":[[2022,9,20]],"date-time":"2022-09-20T15:37:25Z","timestamp":1663688245000},"page":"1-15","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Nominal Matching Logic"],"prefix":"10.1145","author":[{"given":"James","family":"Cheney","sequence":"first","affiliation":[{"name":"University of Edinburgh, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maribel","family":"Fernandez","sequence":"additional","affiliation":[{"name":"KCL, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,9,20]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"crossref","unstructured":"Brian\u00a0E. Aydemir Arthur Chargu\u00e9raud Benjamin\u00a0C. Pierce Randy Pollack and Stephanie Weirich. 2008. Engineering Formal Metatheory. In POPL. 3\u201315.  Brian\u00a0E. Aydemir Arthur Chargu\u00e9raud Benjamin\u00a0C. Pierce Randy Pollack and Stephanie Weirich. 2008. Engineering Formal Metatheory. In POPL. 3\u201315.","DOI":"10.1145\/1328897.1328443"},{"key":"e_1_3_2_1_2_1","first-page":"1","article-title":"Abella: A System for Reasoning about Relational Specifications","volume":"7","author":"Baelde David","year":"2014","unstructured":"David Baelde , Kaustuv Chaudhuri , Andrew Gacek , Dale Miller , Gopalan Nadathur , Alwen Tiu , and Yuting Wang . 2014 a. Abella: A System for Reasoning about Relational Specifications . J. Formalized Reasoning 7 , 2 (2014), 1 \u2013 89 . https:\/\/doi.org\/10.6092\/issn.1972-5787\/4650 10.6092\/issn.1972-5787 David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, and Yuting Wang. 2014a. Abella: A System for Reasoning about Relational Specifications. J. Formalized Reasoning 7, 2 (2014), 1\u201389. https:\/\/doi.org\/10.6092\/issn.1972-5787\/4650","journal-title":"J. Formalized Reasoning"},{"key":"e_1_3_2_1_3_1","first-page":"2","article-title":"Abella: A System for Reasoning about Relational Specifications","volume":"7","author":"Baelde David","year":"2014","unstructured":"David Baelde , Kaustuv Chaudhuri , Andrew Gacek , Dale Miller , Gopalan Nadathur , Alwen Tiu , and Yuting Wang . 2014 b. Abella: A System for Reasoning about Relational Specifications . Journal of Formalized Reasoning 7 , 2 (Jan. 2014), 1\u201389. https:\/\/doi.org\/10.6092\/issn.1972-5787\/4650 10.6092\/issn.1972-5787 David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, and Yuting Wang. 2014b. Abella: A System for Reasoning about Relational Specifications. Journal of Formalized Reasoning 7, 2 (Jan. 2014), 1\u201389. https:\/\/doi.org\/10.6092\/issn.1972-5787\/4650","journal-title":"Journal of Formalized Reasoning"},{"key":"e_1_3_2_1_4_1","volume-title":"21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings(Lecture Notes in Computer Science, Vol.\u00a04603)","author":"Baelde David","year":"2007","unstructured":"David Baelde , Andrew Gacek , Dale Miller , Gopalan Nadathur , and Alwen Tiu . 2007 . The Bedwyr System for Model Checking over Syntactic Expressions. In Automated Deduction - CADE-21 , 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings(Lecture Notes in Computer Science, Vol.\u00a04603) , Frank Pfenning (Ed.). Springer, 391\u2013397. https:\/\/doi.org\/10.1007\/978-3-540-73595-3_28 10.1007\/978-3-540-73595-3_28 David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, and Alwen Tiu. 2007. The Bedwyr System for Model Checking over Syntactic Expressions. In Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings(Lecture Notes in Computer Science, Vol.\u00a04603), Frank Pfenning (Ed.). Springer, 391\u2013397. https:\/\/doi.org\/10.1007\/978-3-540-73595-3_28"},{"key":"e_1_3_2_1_5_1","unstructured":"Henk\u00a0P. Barendregt. 1984. The Lambda Calculus: its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics Vol.\u00a0103. North-Holland.  Henk\u00a0P. Barendregt. 1984. The Lambda Calculus: its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics Vol.\u00a0103. North-Holland."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785675"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408970"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428229"},{"key":"e_1_3_2_1_9_1","volume-title":"FoSSaCS(LNCS, Vol.\u00a03441)","author":"Cheney James","unstructured":"James Cheney . 2005. A Simpler Proof Theory for Nominal Logic . In FoSSaCS(LNCS, Vol.\u00a03441) . Springer , 379\u2013394. James Cheney. 2005. A Simpler Proof Theory for Nominal Logic. In FoSSaCS(LNCS, Vol.\u00a03441). Springer, 379\u2013394."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1140641176"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exu024"},{"key":"e_1_3_2_1_13_1","first-page":"3","article-title":"\u03b1Check: A mechanized metatheory model checker","volume":"17","author":"Cheney James","year":"2017","unstructured":"James Cheney and Alberto Momigliano . 2017 . \u03b1Check: A mechanized metatheory model checker . TPLP 17 , 3 (May 2017), 311\u2013352. James Cheney and Alberto Momigliano. 2017. \u03b1Check: A mechanized metatheory model checker. TPLP 17, 3 (May 2017), 311\u2013352.","journal-title":"TPLP"},{"key":"e_1_3_2_1_14_1","volume-title":"Proceedings of the 20th International Conference on Logic Programming (ICLP 2004)","author":"Cheney James","year":"2004","unstructured":"James Cheney and Christian Urban . 2004 . Alpha-Prolog: A Logic Programming Language with Names, Binding and Alpha-Equivalence . In Proceedings of the 20th International Conference on Logic Programming (ICLP 2004) (LNCS, 3132), Bart Demoenand Vladimir Lifschitz (Eds.). Springer, 269\u2013283. James Cheney and Christian Urban. 2004. Alpha-Prolog: A Logic Programming Language with Names, Binding and Alpha-Equivalence. In Proceedings of the 20th International Conference on Logic Programming (ICLP 2004)(LNCS, 3132), Bart Demoenand Vladimir Lifschitz (Eds.). Springer, 269\u2013283."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1387673.1387675"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1387673.1387675"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Jo\u00eblle Despeyroux Amy\u00a0P. Felty and Andr\u00e9 Hirschowitz. 1995. Higher-Order Abstract Syntax in COQ. In TLCA\u201995(LNCS Vol.\u00a03461). 124\u2013138.  Jo\u00eblle Despeyroux Amy\u00a0P. Felty and Andr\u00e9 Hirschowitz. 1995. Higher-Order Abstract Syntax in COQ. In TLCA\u201995(LNCS Vol.\u00a03461). 124\u2013138.","DOI":"10.1007\/BFb0014049"},{"key":"e_1_3_2_1_18_1","volume-title":"LPAR\u201994(LNCS, Vol.\u00a0822)","author":"Despeyroux Jo\u00eblle","unstructured":"Jo\u00eblle Despeyroux and Andr\u00e9 Hirschowitz . 1994. Higher-Order Abstract Syntax with Induction in COQ . In LPAR\u201994(LNCS, Vol.\u00a0822) . Springer , 159\u2013173. Jo\u00eblle Despeyroux and Andr\u00e9 Hirschowitz. 1994. Higher-Order Abstract Syntax with Induction in COQ. In LPAR\u201994(LNCS, Vol.\u00a0822). Springer, 159\u2013173."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00418-7"},{"key":"e_1_3_2_1_20_1","volume-title":"Semantics Engineering with PLT Redex","author":"Felleisen Matthias","year":"1885","unstructured":"Matthias Felleisen , Robert\u00a0Bruce Findler , and Matthew Flatt . 2009. Semantics Engineering with PLT Redex . MIT Press . http:\/\/mitpress.mit.edu\/catalog\/item\/default.asp?ttype=2&tid=1 1885 Matthias Felleisen, Robert\u00a0Bruce Findler, and Matthew Flatt. 2009. Semantics Engineering with PLT Redex. MIT Press. http:\/\/mitpress.mit.edu\/catalog\/item\/default.asp?ttype=2&tid=11885"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129517000093"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129517000093"},{"key":"e_1_3_2_1_23_1","first-page":"6","article-title":"Nominal","volume":"205","author":"Fern\u00e1ndez Maribel","year":"2007","unstructured":"Maribel Fern\u00e1ndez and Murdoch\u00a0 J. Gabbay . 2007 . Nominal Rewriting. Inf. Comput. 205 , 6 (June 2007), 917\u2013965. Maribel Fern\u00e1ndez and Murdoch\u00a0J. Gabbay. 2007. Nominal Rewriting. Inf. Comput. 205, 6 (June 2007), 917\u2013965.","journal-title":"Rewriting. Inf. Comput."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.10.010"},{"key":"e_1_3_2_1_25_1","first-page":"3","article-title":"A New Approach to Abstract Syntax with Variable Binding","volume":"13","author":"Gabbay J.","year":"2001","unstructured":"Murdoch\u00a0 J. Gabbay and Andrew\u00a0 M. Pitts . 2001 . A New Approach to Abstract Syntax with Variable Binding . Formal Aspects of Computing 13 , 3 \u2013 5 (July 2001), 341\u2013363. Murdoch\u00a0J. Gabbay and Andrew\u00a0M. Pitts. 2001. A New Approach to Abstract Syntax with Variable Binding. Formal Aspects of Computing 13, 3\u20135 (July 2001), 341\u2013363.","journal-title":"Formal Aspects of Computing"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2010.09.004"},{"key":"e_1_3_2_1_27_1","volume-title":"KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine. In CSF 2018","author":"Hildenbrandt Everett","year":"2018","unstructured":"Everett Hildenbrandt , Manasvi Saxena , Nishant Rodrigues , Xiaoran Zhu , Philip Daian , Dwight Guth , Brandon\u00a0 M. Moore , Daejun Park , Yi Zhang , Andrei Stefanescu , and Grigore Rosu . 2018 . KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine. In CSF 2018 . IEEE, 204\u2013217. https:\/\/doi.org\/10.1109\/CSF.2018.00022 10.1109\/CSF.2018.00022 Everett Hildenbrandt, Manasvi Saxena, Nishant Rodrigues, Xiaoran Zhu, Philip Daian, Dwight Guth, Brandon\u00a0M. Moore, Daejun Park, Yi Zhang, Andrei Stefanescu, and Grigore Rosu. 2018. KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine. In CSF 2018. IEEE, 204\u2013217. https:\/\/doi.org\/10.1109\/CSF.2018.00022"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/504077.504080"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094622.1094628"},{"key":"e_1_3_2_1_30_1","volume-title":"Contextual Modal Type Theory. TOCL 9, 3","author":"Nanevski Aleksandar","year":"2008","unstructured":"Aleksandar Nanevski , Frank Pfenning , and Brigitte Pientka . 2008. Contextual Modal Type Theory. TOCL 9, 3 ( 2008 ), 23:1\u201323:49. Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. 2008. Contextual Modal Type Theory. TOCL 9, 3 (2008), 23:1\u201323:49."},{"key":"e_1_3_2_1_31_1","volume-title":"Higher-order Abstract Syntax","author":"Pfenning Frank","unstructured":"Frank Pfenning and Conal Elliott . 1988. Higher-order Abstract Syntax . In PLDI. ACM Press , 199\u2013208. Frank Pfenning and Conal Elliott. 1988. Higher-order Abstract Syntax. In PLDI. ACM Press, 199\u2013208."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328897.1328483"},{"key":"e_1_3_2_1_33_1","volume-title":"Beluga: Programming with Dependent Types, Contextual Data, and Contexts. In FLOPS. 1\u201312. https:\/\/doi.org\/10.1007\/978-3-642-12251-4_1","author":"Pientka Brigitte","year":"2010","unstructured":"Brigitte Pientka . 2010 . Beluga: Programming with Dependent Types, Contextual Data, and Contexts. In FLOPS. 1\u201312. https:\/\/doi.org\/10.1007\/978-3-642-12251-4_1 10.1007\/978-3-642-12251-4_1 Brigitte Pientka. 2010. Beluga: Programming with Dependent Types, Contextual Data, and Contexts. In FLOPS. 1\u201312. https:\/\/doi.org\/10.1007\/978-3-642-12251-4_1"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00138-X"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1147954.1147961"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796811000116"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/2512979"},{"key":"e_1_3_2_1_38_1","volume-title":"Higher-Order Abstract Syntax with Induction in Isabelle\/HOL: Formalizing the pi-Calculus and Mechanizing the Theory of Contexts","author":"R\u00f6ckl Christine","unstructured":"Christine R\u00f6ckl , Daniel Hirschkoff , and Stefan Berghofer . 2001. Higher-Order Abstract Syntax with Induction in Isabelle\/HOL: Formalizing the pi-Calculus and Mechanizing the Theory of Contexts . In FoSSaCS. Springer , 364\u2013378. Christine R\u00f6ckl, Daniel Hirschkoff, and Stefan Berghofer. 2001. Higher-Order Abstract Syntax with Induction in Isabelle\/HOL: Formalizing the pi-Calculus and Mechanizing the Theory of Contexts. In FoSSaCS. Springer, 364\u2013378."},{"key":"e_1_3_2_1_39_1","first-page":"4","article-title":"Matching logic","volume":"13","author":"Ro\u015fu Grigore","year":"2017","unstructured":"Grigore Ro\u015fu . 2017 . Matching logic . Logical Methods in Computer Science 13 , 4 (December 2017), 1\u201361. https:\/\/doi.org\/abs\/1705.06312 Grigore Ro\u015fu. 2017. Matching logic. Logical Methods in Computer Science 13, 4 (December 2017), 1\u201361. https:\/\/doi.org\/abs\/1705.06312","journal-title":"Logical Methods in Computer Science"},{"key":"#cr-split#-e_1_3_2_1_40_1.1","unstructured":"Grigore Rosu. 2017. : A Semantic Framework for Programming Languages and Formal Analysis Tools. In Dependable Software Systems Engineering. 186-206. https:\/\/doi.org\/10.3233\/978-1-61499-810-5-186 10.3233\/978-1-61499-810-5-186"},{"key":"#cr-split#-e_1_3_2_1_40_1.2","unstructured":"Grigore Rosu. 2017. : A Semantic Framework for Programming Languages and Formal Analysis Tools. In Dependable Software Systems Engineering. 186-206. https:\/\/doi.org\/10.3233\/978-1-61499-810-5-186"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990293"},{"key":"e_1_3_2_1_42_1","volume-title":"FreshML: Programmming with Binders Made Simple","author":"Shinwell R.","unstructured":"M.\u00a0 R. Shinwell , A.\u00a0 M. Pitts , and M.\u00a0 J. Gabbay . 2003. FreshML: Programmming with Binders Made Simple . In ICFP. ACM Press , 263\u2013274. M.\u00a0R. Shinwell, A.\u00a0M. Pitts, and M.\u00a0J. Gabbay. 2003. FreshML: Programmming with Binders Made Simple. In ICFP. ACM Press, 263\u2013274."},{"key":"e_1_3_2_1_43_1","first-page":"3","article-title":"A Logic for Reasoning about Generic Judgments","volume":"174","author":"Tiu Alwen","year":"2007","unstructured":"Alwen Tiu . 2007 . A Logic for Reasoning about Generic Judgments . ENTCS 174 , 5 (2007), 3 \u2013 18 . Alwen Tiu. 2007. A Logic for Reasoning about Generic Judgments. ENTCS 174, 5 (2007), 3\u201318.","journal-title":"ENTCS"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-008-9097-2"},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.06.016"}],"event":{"name":"PPDP 2022: 24th International Symposium on Principles and Practice of Declarative Programming","location":"Tbilisi Georgia","acronym":"PPDP 2022"},"container-title":["Proceedings of the 24th International Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3551357.3551375","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3551357.3551375","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:00:24Z","timestamp":1750186824000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3551357.3551375"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,9,20]]},"references-count":45,"alternative-id":["10.1145\/3551357.3551375","10.1145\/3551357"],"URL":"https:\/\/doi.org\/10.1145\/3551357.3551375","relation":{},"subject":[],"published":{"date-parts":[[2022,9,20]]},"assertion":[{"value":"2022-09-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}