{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,20]],"date-time":"2025-10-20T13:41:32Z","timestamp":1760967692510,"version":"build-2065373602"},"reference-count":50,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,8,5]]},"abstract":"<jats:p>\n            Multi-stage programming is a popular approach to typed meta-programming, reducing abstraction overhead and producing performant programs. However, the traditional quote-and-splice staging syntax, as introduced by Rowan Davies in 1996, can introduce complexities in managing expression evaluation, and also often necessitates sophisticated mechanisms for advanced features such as code pattern matching. This paper introduces \u03bb\u25cb\u25b7, a novel staging calculus featuring let-splice bindings, a construct that explicitly binds splice expressions to splice variables, providing flexibility in managing, sharing, and reusing splice computations. Inspired by contextual modal type theory, our type system associates types with a typing context to capture variables dependencies of splice variables. We demonstrate that this mechanism seamlessly scales to features like code pattern matching, by formalizing \u03bb\u25cb\u25b7, an extension of \u03bb\u25cb\u25b7\n            <jats:italic toggle=\"yes\">pat<\/jats:italic>\n            with code pattern matching and rewriting. We establish the syntactic type soundness of both calculi. Furthermore, we define a denotational semantics using a Kripke-style model, and prove adequacy results. All proofs have been fully mechanized using the Agda proof assistant.\n          <\/jats:p>","DOI":"10.1145\/3747518","type":"journal-article","created":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T16:56:02Z","timestamp":1754412962000},"page":"400-434","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Multi-stage Programming with Splice Variables"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1252-6424","authenticated-orcid":false,"given":"Tsung-Ju","family":"Chiang","sequence":"first","affiliation":[{"name":"University of Toronto, Toronto, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5961-1493","authenticated-orcid":false,"given":"Ningning","family":"Xie","sequence":"additional","affiliation":[{"name":"University of Toronto, Toronto, Canada"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,8,5]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796819000170"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","unstructured":"Emmanuel Su\u00e1rez Acevedo and Stephanie Weirich. 2023. Making Logical Relations More Relatable (Proof Pearl). arXiv preprint arXiv:2309.15724 https:\/\/doi.org\/10.48550\/arXiv.2309.15724 10.48550\/arXiv.2309.15724","DOI":"10.48550\/arXiv.2309.15724"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60164-3_27"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2643135.2643146"},{"key":"e_1_2_1_5_1","volume-title":"Proc. Wksp. Scheme and Functional Programming.","author":"Barzilay Eli","year":"2011","unstructured":"Eli Barzilay, Ryan Culpepper, and Matthew Flatt. 2011. Keeping it clean with syntax parameters. Proc. Wksp. Scheme and Functional Programming."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005291931660"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.71.3"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39815-8_4"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","unstructured":"Tsung-Ju Chiang and Ningning Xie. 2025. Multi-Stage Programming with Splice Variables (Artifact). https:\/\/doi.org\/10.5281\/zenodo.15719807 10.5281\/zenodo.15719807","DOI":"10.5281\/zenodo.15719807"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674649"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1317265.1317269"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89366-2_14"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561317"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3011069"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15205-4_26"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2012.07.002"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-17(3:11)2021"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57262-3_3"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704851"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498700"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660241"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54458-7_32"},{"volume-title":"On the Semantics of Intensionality and Intensional Recursion. Ph. D. Dissertation","author":"Kavvos G. A.","key":"e_1_2_1_23_1","unstructured":"G. A. Kavvos. 2017. On the Semantics of Intensionality and Intensional Recursion. Ph. D. Dissertation. University of Oxford."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-16(3:10)2020"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","unstructured":"G. A. Kavvos. 2024. Two-Dimensional Kripke Semantics I: Presheaves. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik 14:1\u201314:23. https:\/\/doi.org\/10.4230\/LIPIcs.FSCD.2024.14 10.4230\/LIPIcs.FSCD.2024.14","DOI":"10.4230\/LIPIcs.FSCD.2024.14"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1017\/bsl.2023.14"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-07151-0_6"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3093333.3009880"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/319838.319859"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2010.09.008"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90067-V"},{"key":"e_1_2_1_32_1","unstructured":"Yuito Murase. 2017. Kripke-style contextual modal type theory. Work-in-progress report at Logical Frameworks and Meta-Languages."},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30044-8_11"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158101"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129501003322"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1868294.1868314"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2184319.2184345"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/581690.581691"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3278122.3278139"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3486609.3487203"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00053-0"},{"key":"e_1_2_1_43_1","unstructured":"The Agda Community. 2024. Agda Standard Library. https:\/\/github.com\/agda\/agda-stdlib"},{"key":"e_1_2_1_44_1","volume-title":"Siek","author":"Wadler Philip","year":"2022","unstructured":"Philip Wadler, Wen Kokke, and Jeremy G. Siek. 2022. Programming Language Foundations in Agda."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341700"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3409002"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498723"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607851"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110273"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591269"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3747518","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,20]],"date-time":"2025-10-20T13:21:24Z","timestamp":1760966484000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3747518"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,5]]},"references-count":50,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2025,8,5]]}},"alternative-id":["10.1145\/3747518"],"URL":"https:\/\/doi.org\/10.1145\/3747518","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2025,8,5]]},"assertion":[{"value":"2025-02-27","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-27","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}