{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T17:23:59Z","timestamp":1787592239020,"version":"build-2736575974"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"funder":[{"DOI":"10.13039\/100016744","name":"Naval Information Warfare Center Pacific","doi-asserted-by":"publisher","award":["NN66001-22-C-4027"],"award-info":[{"award-number":["NN66001-22-C-4027"]}],"id":[{"id":"10.13039\/100016744","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["NN66001-22-C-4027"],"award-info":[{"award-number":["NN66001-22-C-4027"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000038","name":"Natural Sciences and Engineering Research Council of Canada","doi-asserted-by":"publisher","award":["RGPIN-2019-04207"],"award-info":[{"award-number":["RGPIN-2019-04207"]}],"id":[{"id":"10.13039\/501100000038","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":[[2025,4,9]]},"abstract":"<jats:p>\n                    Type-preserving compilation seeks to make\n                    <jats:italic toggle=\"yes\">intent<\/jats:italic>\n                    as much as a part of compilation as\n                    <jats:italic toggle=\"yes\">computation<\/jats:italic>\n                    . Specifications of intent in the form of types are preserved and exploited during compilation and linking, alongside the mere computation of a program. This provides lightweight guarantees for compilation, optimization, and linking. Unfortunately, type-preserving compilation typically interferes with important optimizations. In this paper, we study typed closure representation and optimization. We analyze limitations in prior typed closure conversion representations, and the requirements of many important closure optimizations. We design a new typed closure representation in our Flat-Closure Calculus (FCC) that admits all these optimizations, prove type safety and subject reduction of FCC, prove type preservation from an existing closure converted IR to FCC, and implement common closure optimizations for FCC.\n                  <\/jats:p>","DOI":"10.1145\/3720437","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"649-675","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Type-Preserving Flat Closure Optimization"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-8137-7577","authenticated-orcid":false,"given":"Adam T.","family":"Geller","sequence":"first","affiliation":[{"name":"University of British Columbia, Vancouver, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-5231-8618","authenticated-orcid":false,"given":"Sean","family":"Bocirnea","sequence":"additional","affiliation":[{"name":"University of British Columbia, Vancouver, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-6365-7171","authenticated-orcid":false,"given":"Chester J. F.","family":"Gould","sequence":"additional","affiliation":[{"name":"University of British Columbia, Vancouver, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0325-3305","authenticated-orcid":false,"given":"Paulette","family":"Koronkevich","sequence":"additional","affiliation":[{"name":"University of British Columbia, Vancouver, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6402-4840","authenticated-orcid":false,"given":"William J.","family":"Bowman","sequence":"additional","affiliation":[{"name":"University of British Columbia, Vancouver, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","unstructured":"Amal Ahmed and Matthias Blume. 2008. Typed Closure Conversion Preserves Observational Equivalence. In International Conference on Functional Programming (ICFP). https:\/\/doi.org\/10.1145\/1411204.1411227 10.1145\/1411204.1411227","DOI":"10.1145\/1411204.1411227"},{"key":"e_1_3_1_3_1","volume-title":"Compiling with Continuations","author":"Appel Andrew W.","year":"2006","unstructured":"Andrew W. Appel. 2006. Compiling with Continuations (second ed.). Cambridge University Press."},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","unstructured":"William J. Bowman and Amal Ahmed. 2018. Typed Closure Conversion for the Calculus of Constructions. In International Conference on Programming Language Design and Implementation (PLDI). https:\/\/doi.org\/10.1145\/3192366.3192372 10.1145\/3192366.3192372","DOI":"10.1145\/3192366.3192372"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","unstructured":"Luca Cardelli. 1984. Compiling a functional language. In LISP and Functional Programming (LFP). https:\/\/doi.org\/10.1145\/800055.802037 10.1145\/800055.802037","DOI":"10.1145\/800055.802037"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806612"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","unstructured":"Karl Crary Stephanie Weirich and Greg Morrisett. 2002. Intensional polymorphism in type-erasure semantics. Journal of Functional Programming (JFP) (2002). https:\/\/doi.org\/10.1017\/S0956796801004282 10.1017\/S0956796801004282","DOI":"10.1017\/S0956796801004282"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/37555"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/1795772"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","unstructured":"Adam T. Geller Sean Bocirnea Chester J. F. Gould Paulette Koronkevich and William J. Bowman. 2025. Type-Preserving Flat Closure Optimization Artifact. https:\/\/doi.org\/10.5281\/zenodo.14941604 10.5281\/zenodo.14941604","DOI":"10.5281\/zenodo.14941604"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","unstructured":"Andreas Haas Andreas Rossberg Derek L. Schuff Ben L. Titzer Michael Holman Dan Gohman Luke Wagner Alon Zakai and J. F. Bastien. 2017. Bringing the web up to speed with WebAssembly. In International Conference on Programming Language Design and Implementation (PLDI). https:\/\/doi.org\/10.1145\/3062341.3062363 10.1145\/3062341.3062363","DOI":"10.1145\/3062341.3062363"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(95)00178-6"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/99583.99603"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2661103.2661106"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103691"},{"key":"e_1_3_1_16_1","unstructured":"Andr\u00e1s Kov\u00e1cs. 2018. Closure Conversion for Dependent Type Theory with Type-Passing Polymorphism. In International Workshop on Types for Proofs and Programs (TYPES). https:\/\/github.com\/AndrasKovacs\/misc-stuff\/blob\/master\/MemControl\/types2018\/abstract-types-2018-cconv.pdf"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","unstructured":"Xavier Leroy. 1992. Unboxed objects and polymorphic typing. In Symposium on Principles of Programming Languages (POPL). https:\/\/doi.org\/10.1145\/143165.143205 10.1145\/143165.143205","DOI":"10.1145\/143165.143205"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","unstructured":"Yasuhiko Minamide Greg Morrisett and Robert Harper. 1996a. Typed Closure Conversion. In Symposium on Principles of Programming Languages (POPL). https:\/\/doi.org\/10.1145\/237721.237791 10.1145\/237721.237791","DOI":"10.1145\/237721.237791"},{"key":"e_1_3_1_20_1","doi-asserted-by":"crossref","unstructured":"Yasuhiko Minamide Greg Morrisett and Robert Harper. 1996b. Typed Closure Conversion. techreport. https:\/\/www.cs.cmu.edu\/~rwh\/papers\/closures\/tr.pdf","DOI":"10.1145\/237721.237791"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290325"},{"key":"e_1_3_1_22_1","volume-title":"Compiling with Types","author":"Morrisett Greg","year":"1995","unstructured":"Greg Morrisett. 1995. Compiling with Types. Ph. D. Dissertation. Carnegie Mellon University. https:\/\/www.cs.cmu.edu\/~rwh\/theses\/morrisett.pdf"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/s1571-0661(05)80702-9"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/319301.319345"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","unstructured":"Max S. New William J. Bowman and Amal Ahmed. 2016. Fully Abstract Compilation via Universal Embedding. In International Conference on Functional Programming (ICFP). https:\/\/doi.org\/10.1145\/2951913.2951941 10.1145\/2951913.2951941","DOI":"10.1145\/2951913.2951941"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","unstructured":"Pierre-Marie P\u00e9drot and Nicolas Tabareau. 2020. The fire triangle: how to mix substitution dependent elimination and effects. In Symposium on Principles of Programming Languages (POPL). https:\/\/doi.org\/10.1145\/3371126 10.1145\/3371126","DOI":"10.1145\/3371126"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","unstructured":"Simon L. Peyton Jones. 1996. Compiling Haskell by Program Transformation: A Report from the Trenches. In European Symposium on Programming (ESOP). https:\/\/doi.org\/10.1007\/3-540-61055-3_27 10.1007\/3-540-61055-3_27","DOI":"10.1007\/3-540-61055-3_27"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/509043"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","unstructured":"Manuel Serrano. 1995. Control flow analysis: a functional languages compilation paradigm. In Symposium on Applied Computing (SAC). https:\/\/doi.org\/10.1145\/315891.315934 10.1145\/315891.315934","DOI":"10.1145\/315891.315934"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","unstructured":"Zhong Shao and Andrew W. Appel. 1994. Space-Efficient Closure Representations. In Conference on LISP and Functional Programming (LFP). https:\/\/doi.org\/10.1145\/182409.156783 10.1145\/182409.156783","DOI":"10.1145\/182409.156783"},{"key":"e_1_3_1_31_1","volume-title":"RABBIT: A Compiler for SCHEME (A Study in Compiler Optimization)","author":"Steele Jr Guy Lewis","year":"1978","unstructured":"Guy Lewis Steele Jr. 1978. RABBIT: A Compiler for SCHEME (A Study in Compiler Optimization). Technical Report 474. MIT Artificial Intelligence Lab. https:\/\/dspace.mit.edu\/bitstream\/handle\/1721.1\/6913\/AITR-474.pdf"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","unstructured":"Gordon Stewart Lennart Beringer Santiago Cuellar and Andrew W. Appel. 2015. Compositional CompCert. In Symposium on Principles of Programming Languages (POPL). https:\/\/doi.org\/10.1145\/2676726.2676985 10.1145\/2676726.2676985","DOI":"10.1145\/2676726.2676985"},{"key":"e_1_3_1_33_1","volume-title":"Design and implementation of code optimizations for a type-directed compiler for Standard ML","author":"Tarditi David","year":"1996","unstructured":"David Tarditi. 1996. Design and implementation of code optimizations for a type-directed compiler for Standard ML. Ph. D. Dissertation. Carnegie Mellon University. https:\/\/csd.cmu.edu\/sites\/default\/files\/phd-thesis\/CMU-CS-97-108.pdf"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","unstructured":"David Tarditi Greg Morrisett Perry Cheng Chris Stone Robert Harper and Peter Lee. 1996. TIL: A Type-Directed Optimizing Compiler for ML. In International Conference on Programming Language Design and Implementation (PLDI). https:\/\/doi.org\/10.1145\/231379 10.1145\/231379","DOI":"10.1145\/231379"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55511-0_15"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90050-C"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720437","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720437","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720437","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T16:31:07Z","timestamp":1787589067000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720437"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":36,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720437"],"URL":"https:\/\/doi.org\/10.1145\/3720437","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}