{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T20:12:05Z","timestamp":1760040725394,"version":"build-2065373602"},"publisher-location":"New York, NY, USA","reference-count":40,"publisher":"ACM","license":[{"start":{"date-parts":[[2026,10,9]],"date-time":"2026-10-09T00:00:00Z","timestamp":1791504000000},"content-version":"vor","delay-in-days":365,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF (National Science Foundation)","doi-asserted-by":"publisher","award":["NSF CCF-2327738"],"award-info":[{"award-number":["NSF CCF-2327738"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,10,9]]},"DOI":"10.1145\/3759164.3759348","type":"proceedings-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T19:17:47Z","timestamp":1760037467000},"page":"38-52","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Rebound: Efficient, Expressive, and Well-Scoped Binding"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-5119-3895","authenticated-orcid":false,"given":"No\u00e9","family":"De Santo","sequence":"first","affiliation":[{"name":"University of Pennsylvania, Philadelphia, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6756-9168","authenticated-orcid":false,"given":"Stephanie","family":"Weirich","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, USA"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000186"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.71.1"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000076"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48168-0_32"},{"key":"e_1_3_2_1_5_1","unstructured":"Lennart Augustsson. 2006. \u03bb -calculus cooked four ways."},{"key":"e_1_3_2_1_6_1","volume-title":"Lambda calculi with types","author":"Barendregt H. P.","year":"1985","unstructured":"H. P. Barendregt. 1993. Lambda calculi with types. Oxford University Press, Inc., USA. 117\u2013309. isbn:0198537611"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9219-0"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2503778.2503780"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796899003366"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040306"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411226"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341704"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3406088.3409015"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364506.2364522"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","unstructured":"Gerg\u0151 \u00c9rdi. 2018. Generic Description of Well-Scoped Well-Typed Syntaxes. https:\/\/doi.org\/10.48550\/arXiv.1804.00119 arxiv:1804.00119. 10.48550\/arXiv.1804.00119","DOI":"10.48550\/arXiv.1804.00119"},{"key":"e_1_3_2_1_18_1","unstructured":"Jean-Yves Girard. 1972. Interpr\u00e9tation fonctionnelle et elimination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Universit\u00e9 de Paris 7."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411218"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-59451-5_4"},{"key":"e_1_3_2_1_21_1","unstructured":"Aleksey Kliger and Austin Erlandson. 2014. unbound-generics: Support for programming with names and binders using GHC Generics. https:\/\/github.com\/lambdageek\/unbound-generics"},{"key":"e_1_3_2_1_22_1","unstructured":"Edward A. Kmett. 2013. The bound package. https:\/\/github.com\/ekmett\/bound\/"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCQ60895.2024.10576867"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/6.4.308"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2503778.2503786"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2010-304"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3587216.3587224"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863523.1863529"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607830"},{"key":"e_1_3_2_1_30_1","volume-title":"Dependently Typed Functional Programs and their Proofs. Ph. D. Dissertation","author":"McBride Conor","unstructured":"Conor McBride. 1999. Dependently Typed Functional Programs and their Proofs. Ph. D. Dissertation. University of Edinburgh."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1017472.1017477"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004331"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_24"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289460"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/581690.581691"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294101"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.413"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006557"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","unstructured":"Stephanie Weirich. 2023. Implementing Dependent Types in pi-forall. https:\/\/doi.org\/10.48550\/ARXIV.2207.02129 Lecture notes for the Oregon Programming Languages Summer School 10.48550\/ARXIV.2207.02129","DOI":"10.48550\/ARXIV.2207.02129"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034574.2034818"}],"event":{"name":"Haskell '25: 18th ACM SIGPLAN International Haskell Symposium","location":"Singapore Singapore","acronym":"Haskell '25","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGAda ACM Special Interest Group on Ada Programming Language"]},"container-title":["Proceedings of the 18th ACM SIGPLAN International Haskell Symposium"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3759164.3759348","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3759164.3759348","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T19:29:21Z","timestamp":1760038161000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3759164.3759348"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":40,"alternative-id":["10.1145\/3759164.3759348","10.1145\/3759164"],"URL":"https:\/\/doi.org\/10.1145\/3759164.3759348","relation":{},"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}