{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T03:51:42Z","timestamp":1781927502234,"version":"3.54.5"},"reference-count":78,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"EPSRC","doi-asserted-by":"crossref","award":["EP\/X015114\/1"],"award-info":[{"award-number":["EP\/X015114\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100009708","name":"Novo Nordisk Foundation","doi-asserted-by":"crossref","award":["NNF20OC0063462"],"award-info":[{"award-number":["NNF20OC0063462"]}],"id":[{"id":"10.13039\/501100009708","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Independent Research Fund Denmark","award":["3120-00057B"],"award-info":[{"award-number":["3120-00057B"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>\n                    This paper is a contribution to the meta-theory of systems featuring syntax with bindings, such as \u03bb-calculi and logics. It provides a general criterion that targets\n                    <jats:italic toggle=\"yes\">inductively defined rule-based systems<\/jats:italic>\n                    , enabling for them inductive proofs that leverage\n                    <jats:italic toggle=\"yes\">Barendregt\u2019s variable convention<\/jats:italic>\n                    of keeping the bound and free variables disjoint. It improves on the state of the art by (1) achieving high generality in the style of Knaster-Tarski fixed point definitions (as opposed to imposing syntactic formats), (2) capturing systems of interest without modifications, and (3) accommodating infinitary syntax and non-equivariant predicates.\n                  <\/jats:p>","DOI":"10.1145\/3704893","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"1687-1718","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1560-7326","authenticated-orcid":false,"given":"Jan","family":"van Br\u00fcgge","sequence":"first","affiliation":[{"name":"Heriot-Watt University, Edinburgh, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6745-2560","authenticated-orcid":false,"given":"James","family":"McKinna","sequence":"additional","affiliation":[{"name":"Heriot-Watt University, Edinburgh, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8747-0619","authenticated-orcid":false,"given":"Andrei","family":"Popescu","sequence":"additional","affiliation":[{"name":"University of Sheffield, Sheffield, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7982-2768","authenticated-orcid":false,"given":"Dmitriy","family":"Traytel","sequence":"additional","affiliation":[{"name":"University of Copenhagen, Copenhagen, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_1","unstructured":"2024. The HOL4 Theorem Prover. http:\/\/hol.sourceforge.net\/."},{"key":"e_1_3_2_3_1","article-title":"POPLMark Reloaded","author":"Abel Andreas","year":"2017","unstructured":"Andreas Abel, Alberto Momigliano, and Brigitte Pientka. 2017. POPLMark Reloaded. In Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP) 2017, Marino Miculan and Florian Rabe (Eds.). https:\/\/www.usenix.org\/conference\/osdi21\/presentation\/chajed","journal-title":"Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP) 2017"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236785"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_4"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328443"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.6092\/issn.1972-5787\/4650"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-013-9284-7"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.IC.2008.09.003"},{"key":"e_1_3_2_10_1","volume-title":"The lambda calculus - its syntax and semantics","author":"Barendregt Hendrik Pieter","year":"1985","unstructured":"Hendrik Pieter Barendregt. 1985. The lambda calculus - its syntax and semantics. Studies in logic and the foundations of mathematics, Vol. 103. North-Holland."},{"key":"e_1_3_2_11_1","volume-title":"Formalising process calculi","author":"Bengtson Jesper","year":"2010","unstructured":"Jesper Bengtson. 2010. Formalising process calculi. Ph. D. Dissertation. Uppsala University, Sweden. http:\/\/www.itu.dk\/people\/jebe\/files\/thesis.pdf"},{"key":"e_1_3_2_12_1","article-title":"The pi-calculus in nominal logic","author":"Bengtson Jesper","year":"2012","unstructured":"Jesper Bengtson. 2012. The pi-calculus in nominal logic. Arch. Formal Proofs 2012 (2012). https:\/\/www.isa-afp.org\/entries\/Pi_Calculus.shtml","journal-title":"Arch. Formal Proofs"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00135-2"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.01.018"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290335"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1013"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9225-2"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.2178\/JSL\/1140641176"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001134"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"e_1_3_2_21_1","first-page":"150","volume-title":"Larger infinitary languagesHandbook of Model Theoretic Logics","author":"Dickmann M.","year":"1985","unstructured":"M. Dickmann. 1985. Larger infinitary languages. In Handbook of Model Theoretic Logics. Springer-Verlag, 150\u2013171."},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2287718.2287720"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2312.16239"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1093\/JIGPAL\/JZQ006"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9194-x"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782615"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.IC.2006.10.010"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782617"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650200016"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-019-09522-2"},{"key":"e_1_3_2_31_1","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher Order Logic","author":"Gordon M. J. C.","year":"1993","unstructured":"M. J. C. Gordon and T. F. Melham (Eds.). 1993. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press."},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.2307\/2270356"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_3_2_34_1","unstructured":"John Harrison. 2024. The HOL Light Theorem Prover. http:\/\/www.cl.cam.ac.uk\/~jrh13\/hol-light\/."},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(85)80025-5"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03545-1_9"},{"key":"e_1_3_2_37_1","volume-title":"Reduction Properties of H\u00cfE-Systems","author":"Joachimski Felix","year":"2001","unstructured":"Felix Joachimski. 2001. Reduction Properties of H\u00cfE-Systems. Ph.D. Dissertation. LMU M\u00fcnchen."},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2017.21"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48256-3_11"},{"key":"e_1_3_2_40_1","volume-title":"Model Theory for Infinitary Logic","author":"Keisler H. Jerome","year":"1971","unstructured":"H. Jerome Keisler. 1971. Model Theory for Infinitary Logic. North-Holland Pub. Co., Amsterdam,."},{"key":"e_1_3_2_41_1","article-title":"Un th\u00e9or\u00e8me sur les fonctions d\u2019ensembles","volume":"6","author":"Knaster B.","year":"1928","unstructured":"B. Knaster. 1928. Un th\u00e9or\u00e8me sur les fonctions d\u2019ensembles. Ann. Soc. Polon. Math. 6 (1928), 133-134.","journal-title":"Ann. Soc. Polon. Math"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32784-1_8"},{"key":"e_1_3_2_43_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(4:20)2013"},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0029523"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.2307\/2270908"},{"key":"e_1_3_2_46_1","doi-asserted-by":"crossref","unstructured":"Michael Makkai and Robert Par\u00e9. 1989. Accessible Categories: The Foundations of Categorical Model Theory. Providence.","DOI":"10.1090\/conm\/104"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781316855560"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.57"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006294005493"},{"key":"e_1_3_2_50_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CALCO.2015.336"},{"key":"e_1_3_2_51_1","volume-title":"Communication and Concurrency","author":"Milner R.","year":"1989","unstructured":"R. Milner. 1989. Communication and Concurrency. Prentice-Hall, Inc., USA."},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-58041-3_6"},{"key":"e_1_3_2_53_1","volume-title":"Communicating and Mobile Systems: The \u03c0-Calculus","author":"Milner Robin","year":"1999","unstructured":"Robin Milner. 1999. Communicating and Mobile Systems: The \u03c0-Calculus. Cambridge University Press."},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(92)90008-4"},{"key":"e_1_3_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_2_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30142-4_18"},{"key":"e_1_3_2_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10990-006-8745-7"},{"key":"e_1_3_2_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74591-4_16"},{"key":"e_1_3_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/53990.54010"},{"key":"e_1_3_2_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48660-7_14"},{"key":"e_1_3_2_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12251-4_1"},{"key":"e_1_3_2_62_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00138-X"},{"key":"e_1_3_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/1147954.1147961"},{"key":"e_1_3_2_64_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139084673"},{"key":"e_1_3_2_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-011-9229-Y"},{"key":"e_1_3_2_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290335"},{"key":"e_1_3_2_67_1","first-page":"513","article-title":"Types, Abstraction and Parametric Polymorphism.","author":"Reynolds John C.","year":"1983","unstructured":"John C. Reynolds. 1983. Types, Abstraction and Parametric Polymorphism.. In IFIP Congress. 513\u2013523.","journal-title":"IFIP Congress"},{"key":"e_1_3_2_68_1","doi-asserted-by":"publisher","DOI":"10.1017\/9781316134924"},{"key":"e_1_3_2_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_24"},{"key":"e_1_3_2_70_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1057"},{"key":"e_1_3_2_71_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_3_2_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-008-9097-2"},{"key":"e_1_3_2_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_4"},{"key":"e_1_3_2_74_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(2:14)2012"},{"key":"e_1_3_2_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/1088454.1088458"},{"key":"e_1_3_2_76_1","first-page":"38","article-title":"Nominal Techniques in Isabelle\/HOL","author":"Urban Christian","year":"2005","unstructured":"Christian Urban and Christine Tasson. 2005. Nominal Techniques in Isabelle\/HOL. In CADE. 38\u201353.","journal-title":"CADE"},{"key":"e_1_3_2_77_1","doi-asserted-by":"publisher","unstructured":"Jan van Br\u00fcgge James McKinna Andrei Popescu and Dmitriy Traytel. 2025a. Barendregt Convenes with Knaster and Tarski: Implementation and Mechanization Artifact. https:\/\/doi.org\/10.5281\/zenodo.14197983. 10.5281\/zenodo.14197983.","DOI":"10.5281\/zenodo.14197983."},{"key":"e_1_3_2_78_1","doi-asserted-by":"publisher","unstructured":"Jan van Br\u00fcgge James McKinna Andrei Popescu and Dmitriy Traytel. 2025b. Barendregt Convenes with Knaster and Tarski: Strong Rule Induction for Syntax with Bindings\u2014Technical Report. https:\/\/doi.org\/10.5281\/zenodo.14198069. 10.5281\/zenodo.14198069.","DOI":"10.5281\/zenodo.14198069."},{"key":"e_1_3_2_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99404"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704893","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704893","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:15:32Z","timestamp":1770200132000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704893"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":78,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704893"],"URL":"https:\/\/doi.org\/10.1145\/3704893","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}