{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:17:32Z","timestamp":1770286652231,"version":"3.49.0"},"reference-count":63,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/V002309\/1,EP\/R513180\/1"],"award-info":[{"award-number":["EP\/V002309\/1,EP\/R513180\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,1,16]]},"abstract":"<jats:p>Despite extensive research both on the theoretical and practical fronts, formalising, reasoning about, and implementing languages with variable binding is still a daunting endeavour \u2013 repetitive boilerplate and the overly complicated metatheory of capture-avoiding substitution often get in the way of progressing on to the actually interesting properties of a language. Existing developments offer some relief, however at the expense of inconvenient and error-prone term encodings and lack of formal foundations.<\/jats:p>\n          <jats:p>We present a mathematically-inspired language-formalisation framework implemented in Agda. The system translates the description of a syntax signature with variable-binding operators into an intrinsically-encoded, inductive data type equipped with syntactic operations such as weakening and substitution, along with their correctness properties. The generated metatheory further incorporates metavariables and their associated operation of metasubstitution, which enables second-order equational\/rewriting reasoning. The underlying mathematical foundation of the framework \u2013 initial algebra semantics \u2013 derives compositional interpretations of languages into their models satisfying the semantic substitution lemma by construction.<\/jats:p>","DOI":"10.1145\/3498715","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T17:03:12Z","timestamp":1642006992000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Formal metatheory of second-order abstract syntax"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8558-3492","authenticated-orcid":false,"given":"Marcelo","family":"Fiore","sequence":"first","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5436-6302","authenticated-orcid":false,"given":"Dmitrij","family":"Szamozvancev","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96712"},{"key":"e_1_2_2_2_1","unstructured":"Andreas Abel. 2010. MiniAgda: Integrating Sized and Dependent Types. arxiv:1012.4896. arxiv:1012.4896  Andreas Abel. 2010. MiniAgda: Integrating Sized and Dependent Types. arxiv:1012.4896. arxiv:1012.4896"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796819000170"},{"key":"e_1_2_2_4_1","unstructured":"Peter Aczel. 1978. A General Church\u2013Rosser Theorem. http:\/\/www.ens-lyon.fr\/LIP\/REWRITING\/MISC\/AGeneralChurch-RosserTheorem.pdf Unpublished note.  Peter Aczel. 1978. A General Church\u2013Rosser Theorem. http:\/\/www.ens-lyon.fr\/LIP\/REWRITING\/MISC\/AGeneralChurch-RosserTheorem.pdf Unpublished note."},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000076"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018613"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681500009X"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48168-0_32"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394771"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_4"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328897.1328443"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/c2009-0-14341-6"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(94)00022-0"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9219-0"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796899003366"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290335"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394738"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9225-2"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408970"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411226"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2016.08.025"},{"key":"e_1_2_2_22_1","volume-title":"Reports of the","author":"Day Brian","unstructured":"Brian Day . 1970. On closed categories of functors . In Reports of the Midwest Category Seminar IV. Springer , 1\u201338. Brian Day. 1970. On closed categories of functors. In Reports of the Midwest Category Seminar IV. Springer, 1\u201338."},{"key":"e_1_2_2_23_1","unstructured":"Gerg\u0151 \u00c9rdi. 2018. Generic description of well-scoped well-typed syntaxes. arxiv:1804.00119. arxiv:1804.00119  Gerg\u0151 \u00c9rdi. 2018. Generic description of well-scoped well-typed syntaxes. arxiv:1804.00119. arxiv:1804.00119"},{"key":"e_1_2_2_24_1","volume-title":"On the structure of substitution. https:\/\/www.cl.cam.ac.uk\/~mpf23\/talks\/MFPS2006.pdf Talk at MFPS","author":"Fiore Marcelo","year":"2006","unstructured":"Marcelo Fiore . 2006. On the structure of substitution. https:\/\/www.cl.cam.ac.uk\/~mpf23\/talks\/MFPS2006.pdf Talk at MFPS 2006 . Marcelo Fiore. 2006. On the structure of substitution. https:\/\/www.cl.cam.ac.uk\/~mpf23\/talks\/MFPS2006.pdf Talk at MFPS 2006."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.38"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31585-5_22"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.59"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15205-4_26"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15155-2_33"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782615"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2017.16"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782617"},{"key":"e_1_2_2_33_1","unstructured":"Joseph A. Goguen James W. Thatcher and E. G. Wagner. 1976. An Initial Algebra Approach to the Specification Correctness and Implementation of Abstract Data Types. IBM Research Report 6487 (1976).  Joseph A. Goguen James W. Thatcher and E. G. Wagner. 1976. An Initial Algebra Approach to the Specification Correctness and Implementation of Abstract Data Types. IBM Research Report 6487 (1976)."},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30477-7_23"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/lics.1999.782616"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3437992.3439922"},{"key":"e_1_2_2_37_1","unstructured":"Martin Hyland and Christine Tasson. 2020. The linear-non-linear substitution 2-monad. arxiv:2005.09559. arxiv:2005.09559  Martin Hyland and Christine Tasson. 2020. The linear-non-linear substitution 2-monad. arxiv:2005.09559. arxiv:2005.09559"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167098"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_17"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1446788700010272"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2020.102440"},{"key":"e_1_2_2_42_1","unstructured":"Joachim Lambek. 1980. From \u03bb -calculus to cartesian closed categories. To HB Curry: Essays on Combinatory Logic Lambda Calculus and Formalism 375\u2013402.  Joachim Lambek. 1980. From \u03bb -calculus to cartesian closed categories. To HB Curry: Essays on Combinatory Logic Lambda Calculus and Formalism 375\u2013402."},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_22"},{"key":"e_1_2_2_44_1","unstructured":"The Coq Development Team. 2004. The Coq proof assistant reference manual. https:\/\/coq.inria.fr\/distrib\/current\/files\/CoqRefMan.pdf  The Coq Development Team. 2004. The Coq proof assistant reference manual. https:\/\/coq.inria.fr\/distrib\/current\/files\/CoqRefMan.pdf"},{"key":"e_1_2_2_45_1","unstructured":"Conor McBride. 2005. Type-preserving renaming and substitution. http:\/\/strictlypositive.org\/ren-sub.pdf Unpublished note.  Conor McBride. 2005. Type-preserving renaming and substitution. http:\/\/strictlypositive.org\/ren-sub.pdf Unpublished note."},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1017472.1017477"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1481861.1481862"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/960116.54010"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976002.2976013"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/bf01053036"},{"key":"e_1_2_2_51_1","unstructured":"Andrew M. Pitts. 2019. Initial algebra for a strictly positive endofunctor constructed using sized types and quotient types. https:\/\/www.cl.cam.ac.uk\/~amp12\/agda\/initial-T-algebras\/  Andrew M. Pitts. 2019. Initial algebra for a strictly positive endofunctor constructed using sized types and quotient types. https:\/\/www.cl.cam.ac.uk\/~amp12\/agda\/initial-T-algebras\/"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2020.09.011"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_29"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/944705.944729"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294101"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpaa.2012.09.020"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00170-9"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.aim.2012.06.027"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44612-5_62"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19718-5_25"},{"key":"e_1_2_2_61_1","unstructured":"Vladimir Voevodsky Benedikt Ahrens and Daniel Grayson. 2014. UniMath \u2014 a computer-checked library of univalent mathematics. https:\/\/github.com\/UniMath\/UniMath  Vladimir Voevodsky Benedikt Ahrens and Daniel Grayson. 2014. UniMath \u2014 a computer-checked library of univalent mathematics. https:\/\/github.com\/UniMath\/UniMath"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9230-5"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034818"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498715","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498715","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:28Z","timestamp":1750188628000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498715"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":63,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498715"],"URL":"https:\/\/doi.org\/10.1145\/3498715","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}