{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:45:01Z","timestamp":1780994701039,"version":"3.54.1"},"reference-count":97,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"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\/N019547\/1"],"award-info":[{"award-number":["EP\/N019547\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100010663","name":"H2020 European Research Council","doi-asserted-by":"publisher","award":["713999"],"award-info":[{"award-number":["713999"]}],"id":[{"id":"10.13039\/100010663","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":[[2019,1,2]]},"abstract":"<jats:p>We present a general framework for specifying and reasoning about syntax with bindings. Abstract binder types are modeled using a universe of functors on sets, subject to a number of operations that can be used to construct complex binding patterns and binding-aware datatypes, including non-well-founded and infinitely branching types, in a modular fashion. Despite not committing to any syntactic format, the framework is ``concrete'' enough to provide definitions of the fundamental operators on terms (free variables, alpha-equivalence, and capture-avoiding substitution) and reasoning and definition principles. This work is compatible with classical higher-order logic and has been formalized in the proof assistant Isabelle\/HOL.<\/jats:p>","DOI":"10.1145\/3290335","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-34","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Bindings as bounded natural functors"],"prefix":"10.1145","volume":"3","author":[{"given":"Jasmin Christian","family":"Blanchette","sequence":"first","affiliation":[{"name":"Vrije Universiteit Amsterdam, Netherlands \/ Max Planck Institute for Informatics, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lorenzo","family":"Gheri","sequence":"additional","affiliation":[{"name":"Middlesex University, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrei","family":"Popescu","sequence":"additional","affiliation":[{"name":"Middlesex University, UK \/ Institute of Mathematics at Romanian Academy, Romania"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dmitriy","family":"Traytel","sequence":"additional","affiliation":[{"name":"ETH Zurich, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.06.002"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27764-4_2"},{"key":"e_1_2_2_3_1","volume-title":"Types for Proofs and Programs (TYPES)","author":"Abel Andreas","year":"1999","unstructured":"Andreas Abel and Thorsten Altenkirch . 1999. A Predicative Strong Normalisation Proof for a \u03bb-Calculus with Interleaving Inductive Types . In Types for Proofs and Programs (TYPES) 1999 , Thierry Coquand, Peter Dybjer , Bengt Nordstr\u00f6m, and Jan M. Smith (Eds.). LNCS, Vol. 1956 . Springer , 21\u201340. Andreas Abel and Thorsten Altenkirch. 1999. A Predicative Strong Normalisation Proof for a \u03bb-Calculus with Interleaving Inductive Types. In Types for Proofs and Programs (TYPES) 1999, Thierry Coquand, Peter Dybjer, Bengt Nordstr\u00f6m, and Jan M. Smith (Eds.). LNCS, Vol. 1956. Springer, 21\u201340."},{"key":"e_1_2_2_4_1","volume-title":"Logical Frameworks and MetaLanguages: Theory and Practice (LFMTP)","author":"Abel Andreas","year":"2017","unstructured":"Andreas Abel , Alberto Momigliano , and Brigitte Pientka . 2017. POPLMark Reloaded . In Logical Frameworks and MetaLanguages: Theory and Practice (LFMTP) 2017 , Marino Miculan and Florian Rabe (Eds .). https:\/\/lfmtp.org\/workshops\/ 2017\/inc\/papers\/paper_8_abel.pdf Andreas Abel, Alberto Momigliano, and Brigitte Pientka. 2017. POPLMark Reloaded. In Logical Frameworks and MetaLanguages: 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_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/648332.755560"},{"key":"e_1_2_2_6_1","volume-title":"Computer Science Logic (CSL)","author":"Ahrens Benedikt","year":"2018","unstructured":"Benedikt Ahrens , Andr\u00e9 Hirschowitz , Ambroise Lafont , and Marco Maggesi . 2018. High-Level Signatures and Initial Semantics . In Computer Science Logic (CSL) 2018 , Dan R. Ghica and Achim Jung (Eds.). LIPIcs, Vol. 119 . Schloss Dagstuhl\u2014 Leibniz-Zentrum fuer Informatik , 4:1\u20134:22. Benedikt Ahrens, Andr\u00e9 Hirschowitz, Ambroise Lafont, and Marco Maggesi. 2018. High-Level Signatures and Initial Semantics. In Computer Science Logic (CSL) 2018, Dan R. Ghica and Achim Jung (Eds.). LIPIcs, Vol. 119. Schloss Dagstuhl\u2014 Leibniz-Zentrum fuer Informatik, 4:1\u20134:22."},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236785"},{"key":"e_1_2_2_8_1","doi-asserted-by":"crossref","unstructured":"Thorsten Altenkirch Neil Ghani Peter Hancock Conor McBride and Peter Morris. 2015. Indexed Containers. J. Funct. Program. 25 (2015).  Thorsten Altenkirch Neil Ghani Peter Hancock Conor McBride and Peter Morris. 2015. Indexed Containers. J. Funct. Program. 25 (2015).","DOI":"10.1017\/S095679681500009X"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/647849.737066"},{"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.1016\/j.entcs.2007.01.028"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328443"},{"key":"e_1_2_2_13_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 . Abella: A System for Reasoning about Relational Specifications . J. Formalized Reasoning 7 , 2 (2014), 1 \u2013 89 . David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, and Yuting Wang. 2014. Abella: A System for Reasoning about Relational Specifications. J. Formalized Reasoning 7, 2 (2014), 1\u201389.","journal-title":"J. Formalized Reasoning"},{"key":"e_1_2_2_14_1","volume-title":"The Lambda Calculus: Its Syntax and Semantics. Studies in Logic","author":"Barendregt Henk P.","unstructured":"Henk P. Barendregt . 1984. The Lambda Calculus: Its Syntax and Semantics. Studies in Logic , Vol. 40 . Elsevier . Henk P. Barendregt. 1984. The Lambda Calculus: Its Syntax and Semantics. Studies in Logic, Vol. 40. Elsevier."},{"key":"e_1_2_2_15_1","volume-title":"Combinatorial Species and Tree-Like Structures. Number 67 in Encyclopedia of Mathematics and Its Applications","author":"Bergeron Fran\u00e7ois","unstructured":"Fran\u00e7ois Bergeron , Gilbert Labelle , and Pierre Leroux . 1997. Combinatorial Species and Tree-Like Structures. Number 67 in Encyclopedia of Mathematics and Its Applications . Cambridge University Press . Translated by Margaret Readdy. Fran\u00e7ois Bergeron, Gilbert Labelle, and Pierre Leroux. 1997. Combinatorial Species and Tree-Like Structures. Number 67 in Encyclopedia of Mathematics and Its Applications. Cambridge University Press. Translated by Margaret Readdy."},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.01.018"},{"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":"crossref","unstructured":"Jasmin Christian Blanchette Lorenzo Gheri Andrei Popescu and Dmitriy Traytel. 2019a. Bindings as Bounded Natural Functors (Extended Version). https:\/\/github.com\/dtraytel\/Bindings- as- BNFs\/blob\/master\/bindings_extended.pdf .  Jasmin Christian Blanchette Lorenzo Gheri Andrei Popescu and Dmitriy Traytel. 2019a. Bindings as Bounded Natural Functors (Extended Version). https:\/\/github.com\/dtraytel\/Bindings- as- BNFs\/blob\/master\/bindings_extended.pdf .","DOI":"10.1145\/3290335"},{"key":"e_1_2_2_19_1","unstructured":"Jasmin Christian Blanchette Lorenzo Gheri Andrei Popescu and Dmitriy Traytel. 2019b. Formalization associated with this paper. https:\/\/github.com\/dtraytel\/Bindings- as- BNFs .  Jasmin Christian Blanchette Lorenzo Gheri Andrei Popescu and Dmitriy Traytel. 2019b. Formalization associated with this paper. https:\/\/github.com\/dtraytel\/Bindings- as- BNFs ."},{"key":"e_1_2_2_20_1","volume-title":"Interactive Theorem Proving (ITP)","author":"Blanchette Jasmin Christian","year":"2014","unstructured":"Jasmin Christian Blanchette , Johannes H\u00f6lzl , Andreas Lochbihler , Lorenz Panny , Andrei Popescu , and Dmitriy Traytel . 2014. Truly Modular (Co)datatypes for Isabelle\/HOL. In Interactive Theorem Proving (ITP) 2014 , Gerwin Klein and Ruben Gamboa (Eds.). LNCS, Vol. 8558 . Springer , 93\u2013110. Jasmin Christian Blanchette, Johannes H\u00f6lzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, and Dmitriy Traytel. 2014. Truly Modular (Co)datatypes for Isabelle\/HOL. In Interactive Theorem Proving (ITP) 2014, Gerwin Klein and Ruben Gamboa (Eds.). LNCS, Vol. 8558. Springer, 93\u2013110."},{"key":"e_1_2_2_21_1","volume-title":"Logic in Computer Science (LICS)","author":"Blanchette Jasmin Christian","year":"2017","unstructured":"Jasmin Christian Blanchette , Fabian Meier , Andrei Popescu , and Dmitriy Traytel . 2017. Foundational Nonuniform (Co)datatypes for Higher-Order Logic . In Logic in Computer Science (LICS) 2017 . IEEE Computer Society , 1\u201312. Jasmin Christian Blanchette, Fabian Meier, Andrei Popescu, and Dmitriy Traytel. 2017. Foundational Nonuniform (Co)datatypes for Higher-Order Logic. In Logic in Computer Science (LICS) 2017. IEEE Computer Society, 1\u201312."},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9225-2"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411226"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"e_1_2_2_25_1","volume-title":"Formalisation in Constructive Type Theory of Barendregt\u2019s Variable Convention for Generic Structures with Binders. In Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP)","volume":"274","author":"Copello Ernesto","year":"2018","unstructured":"Ernesto Copello , Nora Szasz , and \u00c1lvaro Tasistro . 2018 . Formalisation in Constructive Type Theory of Barendregt\u2019s Variable Convention for Generic Structures with Binders. In Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP) 2018, Fr\u00e9d\u00e9ric Blanqui and Giselle Reis (Eds.). EPTCS , Vol. 274 . 11\u201326. Ernesto Copello, Nora Szasz, and \u00c1lvaro Tasistro. 2018. Formalisation in Constructive Type Theory of Barendregt\u2019s Variable Convention for Generic Structures with Binders. In Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP) 2018, Fr\u00e9d\u00e9ric Blanqui and Giselle Reis (Eds.). EPTCS, Vol. 274. 11\u201326."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/645892.671587"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9194-x"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9327-3"},{"key":"e_1_2_2_30_1","volume-title":"EPTCS","volume":"185","author":"Felty Amy P.","year":"2015","unstructured":"Amy P. Felty , Alberto Momigliano , and Brigitte Pientka . 2015 b. An Open Challenge Problem Repository for Systems Supporting Binders. In Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP) 2015, Iliano Cervesato and Kaustuv Chaudhuri (Eds.) . EPTCS , Vol. 185 . 18\u201332. Amy P. Felty, Alberto Momigliano, and Brigitte Pientka. 2015b. An Open Challenge Problem Repository for Systems Supporting Binders. In Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP) 2015, Iliano Cervesato and Kaustuv Chaudhuri (Eds.). EPTCS, Vol. 185. 18\u201332."},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_17"},{"key":"e_1_2_2_32_1","volume-title":"Programs Using Syntax with First-Class Binders. In European Symposium on Programming (ESOP)","volume":"10201","author":"Ferreira Francisco","year":"2017","unstructured":"Francisco Ferreira and Brigitte Pientka . 2017 . Programs Using Syntax with First-Class Binders. In European Symposium on Programming (ESOP) 2017, Hongseok Yang (Ed.). LNCS , Vol. 10201 . Springer, 504\u2013529. Francisco Ferreira and Brigitte Pientka. 2017. Programs Using Syntax with First-Class Binders. In European Symposium on Programming (ESOP) 2017, Hongseok Yang (Ed.). LNCS, Vol. 10201. Springer, 504\u2013529."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1112\/jlms\/jdm096"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/788021.788948"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167087"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.10.010"},{"key":"e_1_2_2_37_1","volume-title":"Pitts","author":"Gabbay Murdoch","year":"1999","unstructured":"Murdoch Gabbay and Andrew M . Pitts . 1999 . A New Approach to Abstract Syntax Involving Binders. In Logic in Computer Science (LICS) 1999. IEEE Computer Society , 214\u2013224. Murdoch Gabbay and Andrew M. Pitts. 1999. A New Approach to Abstract Syntax Involving Binders. In Logic in Computer Science (LICS) 1999. IEEE Computer Society, 214\u2013224."},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650200016"},{"key":"e_1_2_2_39_1","volume-title":"Types for Proofs and Programs (TYPES)","author":"Gambino Nicola","year":"2003","unstructured":"Nicola Gambino and Martin Hyland . 2003. Wellfounded Trees and Dependent Polynomial Functors . In Types for Proofs and Programs (TYPES) 2003 , Stefano Berardi, Mario Coppo , and Ferruccio Damiani (Eds.). LNCS, Vol. 3085 . Springer , 210\u2013225. Nicola Gambino and Martin Hyland. 2003. Wellfounded Trees and Dependent Polynomial Functors. In Types for Proofs and Programs (TYPES) 2003, Stefano Berardi, Mario Coppo, and Ferruccio Damiani (Eds.). LNCS, Vol. 3085. Springer, 210\u2013225."},{"key":"e_1_2_2_40_1","volume-title":"Fibrationally. Logical Methods in Computer Science 9, 3","author":"Ghani Neil","year":"2013","unstructured":"Neil Ghani , Patricia Johann , and Cl\u00e9ment Fumex . 2013. Indexed Induction and Coinduction , Fibrationally. Logical Methods in Computer Science 9, 3 ( 2013 ). Neil Ghani, Patricia Johann, and Cl\u00e9ment Fumex. 2013. Indexed Induction and Coinduction, Fibrationally. Logical Methods in Computer Science 9, 3 (2013)."},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-8748-4"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66107-0_16"},{"key":"e_1_2_2_43_1","volume-title":"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 . 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_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1577824.1577827"},{"key":"e_1_2_2_45_1","volume-title":"Plotkin","author":"Harper Robert","year":"1987","unstructured":"Robert Harper , Furio Honsell , and Gordon D . Plotkin . 1987 . A Framework for Defining Logics. In Logic in Computer Science (LICS) 1987. IEEE Computer Society , 194\u2013204. Robert Harper, Furio Honsell, and Gordon D. Plotkin. 1987. A Framework for Defining Logics. In Logic in Computer Science (LICS) 1987. IEEE Computer Society, 194\u2013204."},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.5555\/646234.758793"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.5555\/648335.755741"},{"key":"e_1_2_2_48_1","volume-title":"EPTCS","volume":"77","author":"Hirschowitz Andr\u00e9","year":"2012","unstructured":"Andr\u00e9 Hirschowitz and Marco Maggesi . 2012 . Initial Semantics for Strengthened Signatures. In Fixed Points in Computer Science (FICS) 2012, Dale Miller and Zolt\u00e1n \u00c9sik (Eds.) . EPTCS , Vol. 77 . 31\u201338. Andr\u00e9 Hirschowitz and Marco Maggesi. 2012. Initial Semantics for Strengthened Signatures. In Fixed Points in Computer Science (FICS) 2012, Dale Miller and Zolt\u00e1n \u00c9sik (Eds.). EPTCS, Vol. 77. 31\u201338."},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.5555\/788021.788940"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796899003640"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00264598"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100060734"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/0001-8708(81)90052-9"},{"key":"e_1_2_2_55_1","volume-title":"LNM","volume":"1234","author":"Joyal Andr\u00e9","year":"1986","unstructured":"Andr\u00e9 Joyal . 1986 . Foncteurs analytiques et esp\u00e8ces de structures. In Combinatoire \u00c9num\u00e9rative . LNM , Vol. 1234 . Springer, 126\u2013159. Andr\u00e9 Joyal. 1986. Foncteurs analytiques et esp\u00e8ces de structures. In Combinatoire \u00c9num\u00e9rative. LNM, Vol. 1234. Springer, 126\u2013159."},{"key":"e_1_2_2_56_1","volume-title":"Formal Structures for Computation and Deduction (FSCD)","author":"Kaiser Jonas","year":"2017","unstructured":"Jonas Kaiser , Brigitte Pientka , and Gert Smolka . 2017. Relating System F and \u03bb2: A Case Study in Coq, Abella and Beluga . In Formal Structures for Computation and Deduction (FSCD) 2017 , Dale Miller (Ed.). LIPIcs, Vol. 84 . Schloss Dagstuhl\u2014Leibniz-Zentrum fuer Informatik , 21:1\u201321:19. Jonas Kaiser, Brigitte Pientka, and Gert Smolka. 2017. Relating System F and \u03bb2: A Case Study in Coq, Abella and Beluga. In Formal Structures for Computation and Deduction (FSCD) 2017, Dale Miller (Ed.). LIPIcs, Vol. 84. Schloss Dagstuhl\u2014Leibniz-Zentrum fuer Informatik, 21:1\u201321:19."},{"key":"e_1_2_2_57_1","volume-title":"Studies in Logic and the Foundations of Mathematics","volume":"62","author":"Keisler H. Jerome","year":"1971","unstructured":"H. Jerome Keisler . 1971 . Model Theory for Infinitary Logic: Logic with Countable Conjunctions and Finite Quantifiers . Studies in Logic and the Foundations of Mathematics , Vol. 62 . North Holland. H. Jerome Keisler. 1971. Model Theory for Infinitary Logic: Logic with Countable Conjunctions and Finite Quantifiers. Studies in Logic and the Foundations of Mathematics, Vol. 62. North Holland."},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)00171-5"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364394.2364403"},{"key":"e_1_2_2_60_1","volume-title":"European Symposium on Programming (ESOP)","volume":"9632","author":"Keuchel Steven","year":"2016","unstructured":"Steven Keuchel , Stephanie Weirich , and Tom Schrijvers . 2016 . Needle &amp; Knot: Binder Boilerplate Tied Up . In European Symposium on Programming (ESOP) 2016, Peter Thiemann (Ed.). LNCS , Vol. 9632 . Springer, 419\u2013445. Steven Keuchel, Stephanie Weirich, and Tom Schrijvers. 2016. Needle &amp; Knot: Binder Boilerplate Tied Up. In European Symposium on Programming (ESOP) 2016, Peter Thiemann (Ed.). LNCS, Vol. 9632. Springer, 419\u2013445."},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2013.01.001"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158112"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32784-1_8"},{"key":"e_1_2_2_64_1","volume-title":"Nominal Coalgebraic Data Types with Applications to Lambda Calculus. Logical Methods in Computer Science 9, 4","author":"Kurz Alexander","year":"2013","unstructured":"Alexander Kurz , Daniela Petrisan , Paula Severi , and Fer-Jan de Vries . 2013. Nominal Coalgebraic Data Types with Applications to Lambda Calculus. Logical Methods in Computer Science 9, 4 ( 2013 ). Alexander Kurz, Daniela Petrisan, Paula Severi, and Fer-Jan de Vries. 2013. Nominal Coalgebraic Data Types with Applications to Lambda Calculus. Logical Methods in Computer Science 9, 4 (2013)."},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28869-2_22"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.5555\/647194.720811"},{"key":"e_1_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/1596550.1596571"},{"key":"e_1_2_2_68_1","volume-title":"Accessible Categories: The Foundations of Categorical Model Theory. Contemporary Mathematics","author":"Makkai Michael","year":"1990","unstructured":"Michael Makkai and Robert Par\u00e9 . 1990 . Accessible Categories: The Foundations of Categorical Model Theory. Contemporary Mathematics , Vol. 104 . American Mathematical Society . Michael Makkai and Robert Par\u00e9. 1990. Accessible Categories: The Foundations of Categorical Model Theory. Contemporary Mathematics, Vol. 104. American Mathematical Society."},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.07.025"},{"key":"e_1_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/11546382_3"},{"key":"e_1_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(78)90014-4"},{"key":"e_1_2_2_72_1","volume-title":"Communication and Concurrency","author":"Milner Robin","unstructured":"Robin Milner . 1989. Communication and Concurrency . Prentice Hall . Robin Milner. 1989. Communication and Concurrency. Prentice Hall."},{"key":"e_1_2_2_73_1","volume-title":"Communicating and Mobile Systems: The \u03c0 -Calculus","author":"Milner Robin","unstructured":"Robin Milner . 1999. Communicating and Mobile Systems: The \u03c0 -Calculus . Cambridge University Press . Robin Milner. 1999. Communicating and Mobile Systems: The \u03c0 -Calculus. Cambridge University Press."},{"key":"e_1_2_2_74_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054109006462"},{"key":"e_1_2_2_75_1","volume-title":"Smith","author":"Nordstr\u00f6m Bengt","year":"1990","unstructured":"Bengt Nordstr\u00f6m , Kent Petersson , and Jan M . Smith . 1990 . Programming in Martin-L\u00f6f\u2019s Type Theory: An Introduction. Oxford University Press . Bengt Nordstr\u00f6m, Kent Petersson, and Jan M. Smith. 1990. Programming in Martin-L\u00f6f\u2019s Type Theory: An Introduction. Oxford University Press."},{"key":"e_1_2_2_76_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30142-4_18"},{"key":"e_1_2_2_77_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00248324"},{"key":"e_1_2_2_78_1","doi-asserted-by":"publisher","DOI":"10.1145\/53990.54010"},{"key":"e_1_2_2_79_1","doi-asserted-by":"publisher","DOI":"10.5555\/648235.753634"},{"key":"e_1_2_2_80_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12251-4_1"},{"key":"e_1_2_2_81_1","volume-title":"Types and Programming Languages","author":"Pierce Benjamin C.","unstructured":"Benjamin C. Pierce . 2002. Types and Programming Languages . MIT Press . Benjamin C. Pierce. 2002. Types and Programming Languages. MIT Press."},{"key":"e_1_2_2_82_1","volume-title":"HOL: A Theorem Proving Environment for Higher Order Logic","author":"Pitts A.","year":"1993","unstructured":"A. Pitts . 1993 . In Introduction to HOL: A Theorem Proving Environment for Higher Order Logic . Cambridge University Press, Chapter The HOL Logic , 191\u2013232. A. Pitts. 1993. In Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Chapter The HOL Logic, 191\u2013232."},{"key":"e_1_2_2_83_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00138-X"},{"key":"e_1_2_2_84_1","doi-asserted-by":"publisher","DOI":"10.1145\/1147954.1147961"},{"key":"e_1_2_2_85_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.48"},{"key":"e_1_2_2_86_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.12.120"},{"key":"e_1_2_2_87_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.11.039"},{"key":"e_1_2_2_88_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)00063-5"},{"key":"e_1_2_2_89_1","volume-title":"Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions. In Interactive Theorem Proving (ITP)","author":"Sch\u00e4fer Steven","year":"2015","unstructured":"Steven Sch\u00e4fer , Tobias Tebbi , and Gert Smolka . 2015 . Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions. In Interactive Theorem Proving (ITP) 2015, Christian Urban and Xingyuan Zhang (Eds.). LNCS, Vol. 9236 . Springer , 359\u2013374. Steven Sch\u00e4fer, Tobias Tebbi, and Gert Smolka. 2015. Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions. In Interactive Theorem Proving (ITP) 2015, Christian Urban and Xingyuan Zhang (Eds.). LNCS, Vol. 9236. Springer, 359\u2013374."},{"key":"e_1_2_2_90_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00418-7"},{"key":"e_1_2_2_91_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990293"},{"key":"e_1_2_2_93_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2012.75"},{"key":"e_1_2_2_94_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_41"},{"key":"e_1_2_2_95_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_4"},{"key":"e_1_2_2_96_1","volume-title":"General Bindings and Alpha-Equivalence in Nominal Isabelle. Logical Methods in Computer Science 8, 2","author":"Urban Christian","year":"2012","unstructured":"Christian Urban and Cezary Kaliszyk . 2012. General Bindings and Alpha-Equivalence in Nominal Isabelle. Logical Methods in Computer Science 8, 2 ( 2012 ). Christian Urban and Cezary Kaliszyk. 2012. General Bindings and Alpha-Equivalence in Nominal Isabelle. Logical Methods in Computer Science 8, 2 (2012)."},{"key":"e_1_2_2_97_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_4"},{"key":"e_1_2_2_98_1","doi-asserted-by":"publisher","DOI":"10.1145\/2847538.2847543"},{"key":"e_1_2_2_99_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\/3290335","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290335","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:58:04Z","timestamp":1750208284000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290335"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":97,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290335"],"URL":"https:\/\/doi.org\/10.1145\/3290335","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}