{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T20:55:33Z","timestamp":1770324933875,"version":"3.49.0"},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"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"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>\n            We study nominal recursors from the literature on syntax with bindings and compare them with respect to expressiveness. The term \u201cnominal\u201d refers to the fact that these recursors operate on a syntax representation where the names of bound variables appear explicitly, as in nominal logic. We argue that nominal recursors can be viewed as\n            <jats:italic toggle=\"yes\">epi-recursors<\/jats:italic>\n            , a concept that captures abstractly the distinction between the constructors on which one actually recurses, and other operators and properties that further underpin recursion. We develop an abstract framework for comparing epi-recursors and instantiate it to the existing nominal recursors, and also to several recursors obtained from them by cross-pollination. The resulted expressiveness hierarchies depend on how strictly we perform this comparison, and bring insight into the relative merits of different axiomatizations of syntax. We also apply our methodology to produce an expressiveness hierarchy of nominal\n            <jats:italic toggle=\"yes\">corecursors<\/jats:italic>\n            , which are principles for defining functions targeting infinitary non-well-founded terms (which underlie\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mi>\u03bb<\/mml:mi>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            -calculus semantics concepts such as B\u00f6hm trees). Our results are validated with the Isabelle\/HOL theorem prover.\n          <\/jats:p>","DOI":"10.1145\/3632857","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"425-456","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Nominal Recursors as Epi-Recursors"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8747-0619","authenticated-orcid":false,"given":"Andrei","family":"Popescu","sequence":"first","affiliation":[{"name":"University of Sheffield, Sheffield, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","volume-title":"A-Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP) 2017","author":"Abel Andreas","year":"2017","unstructured":"Andreas Abel, Alberto Momigliano, and Brigitte Pientka. 2017. POPLMark Reloaded.In A-Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP) 2017, Marino Miculan and Florian Rabe (Eds.). https:\/\/lfmtp.org\/workshops\/2017\/inc\/papers\/paper_8_abel.pdf%."},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00728-4"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","unstructured":"Guillaume Allais James Chapman Conor McBride and James McKinna. 2017. Type-and-scope safe programs and their proofs.In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs CPP 2017 Paris France January 16\u201317 2017 Yves Bertot and Viktor Vafeiadis (Eds.). ACM 195\u2013207. https:\/\/doi.org\/10.1145\/3018610.3018613 10.1145\/3018610.3018613.","DOI":"10.1145\/3018610.3018613"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48168-0_32"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/976571.976572"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_4"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.01.028"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328443"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.6092\/issn.1972-5787\/4650"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-013-9284-7"},{"key":"e_1_3_1_12_1","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_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.01.018"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796899003366"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290335"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00024-Q"},{"key":"e_1_3_1_17_1","volume-title":"A course in universal algebra. Graduate Texts in Mathematics","author":"Burris Stanley","year":"1981","unstructured":"Stanley Burris, and Hanamantagouda P. Sankappanavar. 1981. A course in universal algebra. Graduate Texts in Mathematics Vol. 78. Springer."},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9225-2"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","unstructured":"Adam Chlipala. 2008. Parametric Higher-Order Abstract Syntax for Mechanized Semantics.In International Conference on Functional Programming (ICFP) 2008 James Hook and Peter Thiemann (Eds.). ACM 143\u2013156. https:\/\/doi.org\/10.1145\/1411204.1411226 10.1145\/1411204.1411226.","DOI":"10.1145\/1411204.1411226"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.274.2"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014049"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9194-x"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129517000093"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_19"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782615"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782617"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89439-1_11"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129502003912"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09522-2"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0105404"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00260922"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782616"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167098"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48256-3_11"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32784-1_8"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(4:20)2013"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(87)90027-4"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.07.025"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006294005493"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00126-2"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30142-4_18"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74591-4_16"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48660-7_14"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12251-4_1"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1147954.1147961"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139084673"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571210"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-011-9229-Y"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","unstructured":"Andrei Popescu. 2023a. Nominal Recursors as Epi-Recurors (Mechanized Proofs Artifact). Zenodo 2023 https:\/\/doi.org\/10.5281\/zenodo.10116628 10.5281\/zenodo.10116628.","DOI":"10.5281\/zenodo.10116628"},{"key":"e_1_3_1_51_1","unstructured":"Andrei Popescu. 2023b. Nominal Recursors as Epi-Recursors: Extended Technical Report. [arxiv]2301.00894 [cs.LO] https:\/\/arxiv.org\/abs\/2301.00894."},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-023-09672-4"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","unstructured":"Andrei Popescu and Elsa L. Gunter. 2011. Recursion principles for syntax with bindings and substitution. In Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming ICFP 2011 Tokyo Japan September 19\u201321 2011 Manuel M. T. Chakravarty Zhenjiang Hu and Olivier Danvy (Eds.). ACM 346\u2013358. https:\/\/doi.org\/10.1145\/2034773.2034819 10.1145\/2034773.2034819.","DOI":"10.1145\/2034773.2034819"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00418-7"},{"key":"e_1_3_1_55_1","volume-title":"Name-Passing Process Calculi: Operational Models and Structural Operational Semantics","author":"Staton Sam","year":"2007","unstructured":"Sam Staton. 2007. Name-Passing Process Calculi: Operational Models and Structural Operational Semantics. University of Cambridge, Computer Laboratory. https:\/\/www.cl.cam.ac.uk\/techreports\/UCAM-CLTR-688.pdf."},{"key":"e_1_3_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-54233-7_125"},{"key":"e_1_3_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_41"},{"key":"e_1_3_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_4"},{"key":"e_1_3_1_59_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(2:14)2012"},{"key":"e_1_3_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_4"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632857","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632857","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:04:00Z","timestamp":1751659440000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632857"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":59,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632857"],"URL":"https:\/\/doi.org\/10.1145\/3632857","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}