{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:26:06Z","timestamp":1770272766819,"version":"3.49.0"},"reference-count":50,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2018,7,30]],"date-time":"2018-07-30T00:00:00Z","timestamp":1532908800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nd\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,7,30]]},"abstract":"<jats:p>Almost every programming language\u2019s syntax includes a notion of binder and corresponding bound occurrences, along with the accompanying notions of \u03b1-equivalence, capture avoiding substitution, typing contexts, runtime environments, and so on. In the past, implementing and reasoning about programming languages required careful handling to maintain the correct behaviour of bound variables. Modern programming languages include features that enable constraints like scope safety to be expressed in types. Nevertheless, the programmer is still forced to write the same boilerplate over again for each new implementation of a scope safe operation (e.g., renaming, substitution, desugaring, printing, etc.), and then again for correctness proofs.<\/jats:p>\n          <jats:p>We present an expressive universe of syntaxes with binding and demonstrate how to (1) implement scope safe traversals once and for all by generic programming; and (2) how to derive properties of these traversals by generic proving. Our universe description, generic traversals and proofs, and our examples have all been formalised in Agda and are available in the accompanying material.<\/jats:p>\n          <jats:p>NB. we recommend printing the paper in colour to benefit from syntax highlighting in code fragments.<\/jats:p>","DOI":"10.1145\/3236785","type":"journal-article","created":{"date-parts":[[2018,7,31]],"date-time":"2018-07-31T19:41:18Z","timestamp":1533066078000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":22,"title":["A type and scope safe universe of syntaxes with binding: their semantics and proofs"],"prefix":"10.1145","volume":"2","author":[{"given":"Guillaume","family":"Allais","sequence":"first","affiliation":[{"name":"Radboud University Nijmegen, Netherlands"}]},{"given":"Robert","family":"Atkey","sequence":"additional","affiliation":[{"name":"University of Strathclyde, UK"}]},{"given":"James","family":"Chapman","sequence":"additional","affiliation":[{"name":"University of Strathclyde, UK"}]},{"given":"Conor","family":"McBride","sequence":"additional","affiliation":[{"name":"University of Strathclyde, UK"}]},{"given":"James","family":"McKinna","sequence":"additional","affiliation":[{"name":"University of Edinburgh, UK"}]}],"member":"320","published-online":{"date-parts":[[2018,7,30]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/2370077.2370079"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.43.2"},{"key":"e_1_2_2_3_1","volume-title":"POPLMark Reloaded. Proceedings of the Logical Frameworks and Meta-Languages: Theory and Practice Workshop","author":"Abel Andreas","year":"2017","unstructured":"Andreas Abel , Alberto Momigliano , and Brigitte Pientka . 2017 . POPLMark Reloaded. Proceedings of the Logical Frameworks and Meta-Languages: Theory and Practice Workshop (2017). Andreas Abel, Alberto Momigliano, and Brigitte Pientka. 2017. POPLMark Reloaded. Proceedings of the Logical Frameworks and Meta-Languages: Theory and Practice Workshop (2017)."},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2480359.2429075"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3018610.3018613"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12032-9_21"},{"key":"e_1_2_2_7_1","first-page":"1","article-title":"Relative Monads Formalised","volume":"7","author":"Altenkirch Thorsten","year":"2014","unstructured":"Thorsten Altenkirch , James Chapman , and Tarmo Uustalu . 2014 . Relative Monads Formalised . Journal of Formalized Reasoning 7 , 1 (2014), 1 \u2013 43 . Thorsten Altenkirch, James Chapman, and Tarmo Uustalu. 2014. Relative Monads Formalised. Journal of Formalized Reasoning 7, 1 (2014), 1\u201343.","journal-title":"Journal of Formalized Reasoning"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/648334.755596"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/647100.717294"},{"key":"e_1_2_2_10_1","volume-title":"Monadic presentations of lambda terms using generalized inductive types","author":"Altenkirch Thorsten","unstructured":"Thorsten Altenkirch and Bernhard Reus . 1999. Monadic presentations of lambda terms using generalized inductive types . In CSL. Springer , 453\u2013468. Thorsten Altenkirch and Bernhard Reus. 1999. Monadic presentations of lambda terms using generalized inductive types. In CSL. Springer, 453\u2013468."},{"key":"e_1_2_2_11_1","unstructured":"Robert Atkey. 2015. An Algebraic Approach to Typechecking and Elaboration. (2015). http:\/\/bentnib.org\/posts\/ 2015-04-19-algebraic-approach-typechecking-and-elaboration.html  Robert Atkey. 2015. An Algebraic Approach to Typechecking and Elaboration. (2015). http:\/\/bentnib.org\/posts\/ 2015-04-19-algebraic-approach-typechecking-and-elaboration.html"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11541868_4"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158104"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(94)00022-0"},{"key":"e_1_2_2_15_1","first-page":"4","article-title":"Universes for Generic Programs and Proofs in Dependent Type Theory","volume":"10","author":"Benke Marcin","year":"2003","unstructured":"Marcin Benke , Peter Dybjer , and Patrik Jansson . 2003 . Universes for Generic Programs and Proofs in Dependent Type Theory . Nordic J. of Computing 10 , 4 (Dec. 2003), 265\u2013289. http:\/\/dl.acm.org\/citation.cfm?id=985799.985801 Marcin Benke, Peter Dybjer, and Patrik Jansson. 2003. Universes for Generic Programs and Proofs in Dependent Type Theory. Nordic J. of Computing 10, 4 (Dec. 2003), 265\u2013289. http:\/\/dl.acm.org\/citation.cfm?id=985799.985801","journal-title":"Nordic J. of Computing"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9219-0"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796899003366"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863547"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9225-2"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411203.1411226"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1019964114625"},{"key":"e_1_2_2_25_1","volume-title":"Indagationes Mathematicae","author":"de Bruijn Nicolaas Govert","unstructured":"Nicolaas Govert de Bruijn . 1972. Lambda Calculus Notation with Nameless Dummies . In Indagationes Mathematicae , Vol. 75 . Elsevier , 381\u2013392. Nicolaas Govert de Bruijn. 1972. Lambda Calculus Notation with Nameless Dummies. In Indagationes Mathematicae, Vol. 75. Elsevier, 381\u2013392."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21401-6_26"},{"key":"e_1_2_2_27_1","volume-title":"Inductive families. Formal aspects of computing 6, 4","author":"Dybjer Peter","year":"1994","unstructured":"Peter Dybjer . 1994. Inductive families. Formal aspects of computing 6, 4 ( 1994 ), 440\u2013465. Peter Dybjer. 1994. Inductive families. Formal aspects of computing 6, 4 (1994), 440\u2013465."},{"key":"e_1_2_2_28_1","volume-title":"A Finite Axiomatization of Inductive-Recursive Definitions","author":"Dybjer Peter","unstructured":"Peter Dybjer and Anton Setzer . 1999. A Finite Axiomatization of Inductive-Recursive Definitions . Springer , 129\u2013146. Peter Dybjer and Anton Setzer. 1999. A Finite Axiomatization of Inductive-Recursive Definitions. Springer, 129\u2013146."},{"key":"e_1_2_2_29_1","unstructured":"Gerg\u0151 \u00c9rdi. 2018. Generic description of well-scoped well-typed syntaxes. (2018). https:\/\/github.com\/gergoerdi\/ universe-of-syntax Unpublished draft privately communicated.  Gerg\u0151 \u00c9rdi. 2018. Generic description of well-scoped well-typed syntaxes. (2018). https:\/\/github.com\/gergoerdi\/ universe-of-syntax Unpublished draft privately communicated."},{"key":"e_1_2_2_30_1","volume-title":"Proc. 14 th LICS Conf. IEEE, Computer Society Press, 193\u2013202","author":"Fiore Marcelo","year":"1999","unstructured":"Marcelo Fiore , Gordon Plotkin , and Daniele Turi . 1999 . Abstract Syntax and Variable Binding (Extended Abstract) . In Proc. 14 th LICS Conf. IEEE, Computer Society Press, 193\u2013202 . Marcelo Fiore, Gordon Plotkin, and Daniele Turi. 1999. Abstract Syntax and Variable Binding (Extended Abstract). In Proc. 14 th LICS Conf. IEEE, Computer Society Press, 193\u2013202."},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650200016"},{"key":"e_1_2_2_32_1","volume-title":"Proc. of 7th Symp. on Trends in Functional Programming, TFP","volume":"2006","author":"Ghani Neil","year":"2006","unstructured":"Neil Ghani , Makoto Hamana , Tarmo Uustalu , and Varmo Vene . 2006 . Representing cyclic structures as nested datatypes . In Proc. of 7th Symp. on Trends in Functional Programming, TFP , Vol. 2006 . Neil Ghani, Makoto Hamana, Tarmo Uustalu, and Varmo Vene. 2006. Representing cyclic structures as nested datatypes. In Proc. of 7th Symp. on Trends in Functional Programming, TFP , Vol. 2006."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02273-9_11"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/242224.242477"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002864"},{"key":"e_1_2_2_36_1","unstructured":"Alan Jeffrey. 2011. Associativity for free! http:\/\/thread.gmane.org\/gmane.comp.lang.agda\/3259 . (2011).  Alan Jeffrey. 2011. Associativity for free! http:\/\/thread.gmane.org\/gmane.comp.lang.agda\/3259 . (2011)."},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167098"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544174.2500618"},{"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.1007\/978-3-642-28869-2_22"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"e_1_2_2_42_1","unstructured":"The Coq Development Team. 2017. The Coq proof assistant reference manual. \u03c0 r 2 Team. http:\/\/coq.inria.fr Version 8.6.  The Coq Development Team. 2017. The Coq proof assistant reference manual. \u03c0 r 2 Team. http:\/\/coq.inria.fr Version 8.6."},{"key":"e_1_2_2_43_1","unstructured":"Conor McBride. 2017. Ornamental algebras algebraic ornaments. (2017). https:\/\/personal.cis.strath.ac.uk\/conor.mcbride\/ pub\/OAAO\/Ornament.pdf  Conor McBride. 2017. Ornamental algebras algebraic ornaments. (2017). https:\/\/personal.cis.strath.ac.uk\/conor.mcbride\/ pub\/OAAO\/Ornament.pdf"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006326"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167081"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90067-V"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/11617990_16"},{"key":"e_1_2_2_48_1","volume-title":"AFP Summer School","author":"Norell Ulf","unstructured":"Ulf Norell . 2009. Dependently typed programming in Agda . In AFP Summer School . Springer , 230\u2013266. Ulf Norell. 2009. Dependently typed programming in Agda. In AFP Summer School. Springer, 230\u2013266."},{"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.1145\/345099.345100"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_29"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006758"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3236785","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3236785","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T21:41:28Z","timestamp":1750282888000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3236785"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,7,30]]},"references-count":50,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2018,7,30]]}},"alternative-id":["10.1145\/3236785"],"URL":"https:\/\/doi.org\/10.1145\/3236785","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,7,30]]},"assertion":[{"value":"2018-07-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}