{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:12:46Z","timestamp":1775873566873,"version":"3.50.1"},"reference-count":84,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T00:00:00Z","timestamp":1697414400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1553471, 1564207, 1918483, 1910216"],"award-info":[{"award-number":["1553471, 1564207, 1918483, 1910216"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000015","name":"DOE U.S. Department of Energy","doi-asserted-by":"publisher","award":["DE-SC0018050"],"award-info":[{"award-number":["DE-SC0018050"]}],"id":[{"id":"10.13039\/100000015","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":[[2023,10,16]]},"abstract":"<jats:p>Graph-based intermediate representations (IRs) are widely used for powerful compiler optimizations, either interprocedurally in pure functional languages, or intraprocedurally in imperative languages. Yet so far, no suitable graph IR exists for aggressive global optimizations in languages with both effects and higher-order functions: aliasing and indirect control transfers make it difficult to maintain sufficiently granular dependency information for optimizations to be effective. To close this long-standing gap, we propose a novel typed graph IR combining a notion of reachability types with an expressive effect system to compute precise and granular effect dependencies at an affordable cost while supporting local reasoning and separate compilation. Our high-level graph IR imposes lexical structure to represent structured control flow and nesting, enabling aggressive and yet inexpensive code motion and other optimizations for impure higher-order programs. We formalize the new graph IR based on a \u03bb-calculus with a reachability type-and-effect system along with a specification of various optimizations. We present performance case studies for tensor loop fusion, CUDA kernel fusion, symbolic execution of LLVM IR, and SQL query compilation in the Scala LMS compiler framework using the new graph IR. We observe significant speedups of up to 21<jats:italic>x<\/jats:italic>.<\/jats:p>","DOI":"10.1145\/3622813","type":"journal-article","created":{"date-parts":[[2023,10,16]],"date-time":"2023-10-16T15:41:29Z","timestamp":1697470889000},"page":"400-430","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":11,"title":["Graph IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Affordable with Precise Effect Dependencies"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3569-4869","authenticated-orcid":false,"given":"Oliver","family":"Bra\u010devac","sequence":"first","affiliation":[{"name":"Purdue University, West Lafayette, USA \/ Galois, Inc., Portland, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3150-2033","authenticated-orcid":false,"given":"Guannan","family":"Wei","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-2526-0438","authenticated-orcid":false,"given":"Songlin","family":"Jia","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6054-2432","authenticated-orcid":false,"given":"Supun","family":"Abeysinghe","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-2610-4743","authenticated-orcid":false,"given":"Yuxuan","family":"Jiang","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3832-3134","authenticated-orcid":false,"given":"Yuyan","family":"Bao","sequence":"additional","affiliation":[{"name":"Augusta University, Augusta, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2068-3238","authenticated-orcid":false,"given":"Tiark","family":"Rompf","sequence":"additional","affiliation":[{"name":"Purdue University, West Lafayette, USA"}]}],"member":"320","published-online":{"date-parts":[[2023,10,16]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proc. ACM Program. Lang., 5, OOPSLA","author":"Bao Yuyan","year":"2021","unstructured":"Yuyan Bao , Guannan Wei , Oliver Bra\u010devac , Yuxuan Jiang , Qiyang He , and Tiark Rompf . 2021 . Reachability Types: Tracking Aliasing and Separation in Higher-Order Functional Programs . Proc. ACM Program. Lang., 5, OOPSLA (2021), 139:1\u2013139:32. Yuyan Bao, Guannan Wei, Oliver Bra\u010devac, Yuxuan Jiang, Qiyang He, and Tiark Rompf. 2021. Reachability Types: Tracking Aliasing and Separation in Higher-Order Functional Programs. Proc. ACM Program. Lang., 5, OOPSLA (2021), 139:1\u2013139:32."},{"key":"e_1_2_1_2_1","unstructured":"Yuyan Bao Guannan Wei Oliver Bra\u010devac and Tiark Rompf. 2023. Modeling Reachability Types with Logical Relations: Semantic Type Soundness Termination and Equational Theory. arxiv:2309.05885. Yuyan Bao Guannan Wei Oliver Bra\u010devac and Tiark Rompf. 2023. Modeling Reachability Types with Logical Relations: Semantic Type Soundness Termination and Equational Theory. arxiv:2309.05885."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37051-9_2"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-17945-3_8"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1599410.1599447"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11924661_7"},{"key":"e_1_2_1_7_1","unstructured":"Oliver Bra\u010devac Guannan Wei Songlin Jia Supun Abeysinghe Yuxuan Jiang Yuyan Bao and Tiark Rompf. 2023. Graph IRs for Impure Higher-Order Languages (Technical Report). arxiv:2309.08118. Oliver Bra\u010devac Guannan Wei Songlin Jia Supun Abeysinghe Yuxuan Jiang Yuyan Bao and Tiark Rompf. 2023. Graph IRs for Impure Higher-Order Languages (Technical Report). arxiv:2309.08118."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36946-9_3"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/207110.207154"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/202529.202534"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115320"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/512644.512651"},{"key":"e_1_2_1_13_1","first-page":"1","article-title":"Lambda-dropping: transforming recursive equations into programs with block structure","volume":"248","author":"Danvy Olivier","year":"2000","unstructured":"Olivier Danvy and Ulrik Pagh Schultz . 2000 . Lambda-dropping: transforming recursive equations into programs with block structure . Theor. Comput. Sci. , 248 , 1 - 2 (2000), 243\u2013287. Olivier Danvy and Ulrik Pagh Schultz. 2000. Lambda-dropping: transforming recursive equations into programs with block structure. Theor. Comput. Sci., 248, 1-2 (2000), 243\u2013287.","journal-title":"Theor. Comput. Sci."},{"key":"e_1_2_1_14_1","first-page":"2004","volume-title":"Funct. Log. Program.","author":"Danvy Olivier","year":"2004","unstructured":"Olivier Danvy and Ulrik Pagh Schultz . 2004 . Lambda-Lifting in Quadratic Time. J . Funct. Log. Program. , 2004 (2004). Olivier Danvy and Ulrik Pagh Schultz. 2004. Lambda-Lifting in Quadratic Time. J. Funct. Log. Program., 2004 (2004)."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2528932"},{"key":"e_1_2_1_16_1","doi-asserted-by":"crossref","unstructured":"Stephen Dolan and Alan Mycroft. 2017. Polymorphism subtyping and type inference in MLsub. In POPL. ACM 60\u201372. Stephen Dolan and Alan Mycroft. 2017. Polymorphism subtyping and type inference in MLsub. In POPL. ACM 60\u201372.","DOI":"10.1145\/3093333.3009882"},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the Asia-Pacific Programming Languages and Compilers Workshop.","author":"Duboscq Gilles","year":"2013","unstructured":"Gilles Duboscq , Lukas Stadler , Thomas W\u00fcrthinger , Doug Simon , Christian Wimmer , and Hanspeter M\u00f6ssenb\u00f6ck . 2013 . Graal IR: An extensible declarative intermediate representation . In Proceedings of the Asia-Pacific Programming Languages and Compilers Workshop. Gilles Duboscq, Lukas Stadler, Thomas W\u00fcrthinger, Doug Simon, Christian Wimmer, and Hanspeter M\u00f6ssenb\u00f6ck. 2013. Graal IR: An extensible declarative intermediate representation. In Proceedings of the Asia-Pacific Programming Languages and Compilers Workshop."},{"key":"e_1_2_1_18_1","volume-title":"98:1\u201398:38","author":"Dunfield Jana","year":"2022","unstructured":"Jana Dunfield and Neel Krishnaswami . 2022. Bidirectional Typing . ACM Comput . Surv., 54, 5 ( 2022 ), 98:1\u201398:38 . Jana Dunfield and Neel Krishnaswami. 2022. Bidirectional Typing. ACM Comput. Surv., 54, 5 (2022), 98:1\u201398:38."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796802004574"},{"key":"e_1_2_1_20_1","volume-title":"Flare: Optimizing Apache Spark with Native Compilation for Scale-Up Architectures and Medium-Size Data","author":"Essertel Gr\u00e9gory M.","year":"2018","unstructured":"Gr\u00e9gory M. Essertel , Ruby Y. Tahboub , James M. Decker , Kevin J. Brown , Kunle Olukotun , and Tiark Rompf . 2018 . Flare: Optimizing Apache Spark with Native Compilation for Scale-Up Architectures and Medium-Size Data . In OSDI. USENIX Association , 799\u2013815. Gr\u00e9gory M. Essertel, Ruby Y. Tahboub, James M. Decker, Kevin J. Brown, Kunle Olukotun, and Tiark Rompf. 2018. Flare: Optimizing Apache Spark with Native Compilation for Scale-Up Architectures and Medium-Size Data. In OSDI. USENIX Association, 799\u2013815."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/24039.24041"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11227-015-1483-z"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155113"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3450272"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408974"},{"key":"e_1_2_1_26_1","volume-title":"A Generic Account of Continuation-Passing Styles","author":"Hatcliff John","unstructured":"John Hatcliff and Olivier Danvy . 1994. A Generic Account of Continuation-Passing Styles . In POPL. ACM Press , 458\u2013471. John Hatcliff and Olivier Danvy. 1994. A Generic Account of Continuation-Passing Styles. In POPL. ACM Press, 458\u2013471."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062354"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411243"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/502874.502880"},{"key":"e_1_2_1_30_1","volume-title":"FPCA (Lecture Notes in Computer Science","volume":"203","author":"Johnsson Thomas","year":"1985","unstructured":"Thomas Johnsson . 1985 . Lambda Lifting: Treansforming Programs to Recursive Equations . In FPCA (Lecture Notes in Computer Science , Vol. 201). Springer, 190\u2013 203 . Thomas Johnsson. 1985. Lambda Lifting: Treansforming Programs to Recursive Equations. In FPCA (Lecture Notes in Computer Science, Vol. 201). Springer, 190\u2013203."},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3418295"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/319301.319348"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/143095.143136"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/143095.143136"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/183432.183443"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/CGO.2004.1281665"},{"key":"e_1_2_1_37_1","volume-title":"MLIR: Scaling Compiler Infrastructure for Domain Specific Computation","author":"Lattner Chris","year":"2021","unstructured":"Chris Lattner , Mehdi Amini , Uday Bondhugula , Albert Cohen , Andy Davis , Jacques A. Pienaar , River Riddle , Tatiana Shpeisman , Nicolas Vasilache , and Oleksandr Zinenko . 2021 . MLIR: Scaling Compiler Infrastructure for Domain Specific Computation . In CGO. IEEE , 2\u201314. Chris Lattner, Mehdi Amini, Uday Bondhugula, Albert Cohen, Andy Davis, Jacques A. Pienaar, River Riddle, Tatiana Shpeisman, Nicolas Vasilache, and Oleksandr Zinenko. 2021. MLIR: Scaling Compiler Infrastructure for Domain Specific Computation. In CGO. IEEE, 2\u201314."},{"key":"e_1_2_1_38_1","volume-title":"A graph-based higher-order intermediate representation","author":"Roland Lei\u00df","unstructured":"Roland Lei\u00df a, Marcel K\u00f6ster , and Sebastian Hack . 2015. A graph-based higher-order intermediate representation . In CGO. IEEE Computer Society , 202\u2013212. Roland Lei\u00df a, Marcel K\u00f6ster, and Sebastian Hack. 2015. A graph-based higher-order intermediate representation. In CGO. IEEE Computer Society, 202\u2013212."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2663171.2663188"},{"key":"e_1_2_1_40_1","volume-title":"Control-flow analysis of functional programs. ACM Comput. Surv., 44, 3","author":"Midtgaard Jan","year":"2012","unstructured":"Jan Midtgaard . 2012. Control-flow analysis of functional programs. ACM Comput. Surv., 44, 3 ( 2012 ), 10:1\u201310:33. Jan Midtgaard. 2012. Control-flow analysis of functional programs. ACM Comput. Surv., 44, 3 (2012), 10:1\u201310:33."},{"key":"e_1_2_1_42_1","doi-asserted-by":"crossref","unstructured":"Matthew Might Yannis Smaragdakis and David Van Horn. 2010. Resolving and exploiting the k-CFA paradox: illuminating functional vs. object-oriented program analysis. In PLDI. ACM 305\u2013315. Matthew Might Yannis Smaragdakis and David Van Horn. 2010. Resolving and exploiting the k-CFA paradox: illuminating functional vs. object-oriented program analysis. In PLDI. ACM 305\u2013315.","DOI":"10.1145\/1809028.1806631"},{"key":"e_1_2_1_43_1","volume-title":"Moraz\u00e1n and Ulrik Pagh Schultz","author":"Marco","year":"2007","unstructured":"Marco T. Moraz\u00e1n and Ulrik Pagh Schultz . 2007 . Optimal Lambda Lifting in Quadratic Time. In IFL (Lecture Notes in Computer Science , Vol. 5083). Springer, 37\u2013 56 . Marco T. Moraz\u00e1n and Ulrik Pagh Schultz. 2007. Optimal Lambda Lifting in Quadratic Time. In IFL (Lecture Notes in Computer Science, Vol. 5083). Springer, 37\u201356."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/322186.322198"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.14778\/2002938.2002940"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054091"},{"key":"e_1_2_1_47_1","volume-title":"Putting Type Annotations to Work","author":"Odersky Martin","unstructured":"Martin Odersky and Konstantin L\u00e4ufer . 1996. Putting Type Annotations to Work . In POPL. ACM Press , 54\u201367. Martin Odersky and Konstantin L\u00e4ufer. 1996. Putting Type Annotations to Work. In POPL. ACM Press, 54\u201367."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1096-9942(199901\/03)5:1<35::AID-TAPO4>3.0.CO;2-4"},{"key":"e_1_2_1_49_1","doi-asserted-by":"crossref","unstructured":"Martin Odersky Christoph Zenger and Matthias Zenger. 2001. Colored local type inference. In POPL. ACM 41\u201353. Martin Odersky Christoph Zenger and Matthias Zenger. 2001. Colored local type inference. In POPL. ACM 41\u201353.","DOI":"10.1145\/373243.360207"},{"key":"e_1_2_1_50_1","volume-title":"Proceedings of the Java Virtual Machine Research and Technology Symposium. 1, 1\u201312","author":"Paleczny Michael","year":"2001","unstructured":"Michael Paleczny , Christopher Vick , and Cliff Click . 2001 . The Java HotSpot^ tm Server Compiler . In Proceedings of the Java Virtual Machine Research and Technology Symposium. 1, 1\u201312 . Michael Paleczny, Christopher Vick, and Cliff Click. 2001. The Java HotSpot^ tm Server Compiler. In Proceedings of the Java Virtual Machine Research and Technology Symposium. 1, 1\u201312."},{"key":"e_1_2_1_51_1","volume-title":"Proc. ACM Program. Lang., 4, ICFP","author":"Parreaux Lionel","year":"2020","unstructured":"Lionel Parreaux . 2020 . The simple essence of algebraic subtyping: principal type inference with subtyping made easy (functional pearl) . Proc. ACM Program. Lang., 4, ICFP (2020), 124:1\u2013124:28. Lionel Parreaux. 2020. The simple essence of algebraic subtyping: principal type inference with subtyping made easy (functional pearl). Proc. ACM Program. Lang., 4, ICFP (2020), 124:1\u2013124:28."},{"key":"e_1_2_1_52_1","volume-title":"The Implementation of Functional Programming Languages","author":"Peyton-Jones Simon L.","unstructured":"Simon L. Peyton-Jones . 1987. The Implementation of Functional Programming Languages . Prentice-Hall . Simon L. Peyton-Jones. 1987. The Implementation of Functional Programming Languages. Prentice-Hall."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/99370.99385"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3211346.3211348"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30936-1_17"},{"key":"e_1_2_1_59_1","doi-asserted-by":"crossref","unstructured":"Tiark Rompf and Nada Amin. 2015. Functional pearl: a SQL to C compiler in 500 lines of code. In ICFP. ACM 2\u20139. Tiark Rompf and Nada Amin. 2015. Functional pearl: a SQL to C compiler in 500 lines of code. In ICFP. ACM 2\u20139.","DOI":"10.1145\/2858949.2784760"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/1868294.1868314"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429128"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.66.5"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341701"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/53990.54007"},{"key":"e_1_2_1_66_1","doi-asserted-by":"crossref","unstructured":"Olin Shivers. 2004. Higher-Order Control-Flow Analysis in Retrospect: Lessons Learned Lessons Abandoned. In Best of PLDI. ACM 257\u2013269. Olin Shivers. 2004. Higher-Order Control-Flow Analysis in Retrospect: Lessons Learned Lessons Abandoned. In Best of PLDI. ACM 257\u2013269.","DOI":"10.1145\/989393.989421"},{"key":"e_1_2_1_67_1","volume-title":"Partial Escape Analysis and Scalar Replacement for Java. In 12th Annual IEEE\/ACM International Symposium on Code Generation and Optimization, CGO 2014","author":"Stadler Lukas","year":"2014","unstructured":"Lukas Stadler , Thomas W\u00fcrthinger , and Hanspeter M\u00f6ssenb\u00f6ck . 2014 . Partial Escape Analysis and Scalar Replacement for Java. In 12th Annual IEEE\/ACM International Symposium on Code Generation and Optimization, CGO 2014 , Orlando, FL, USA , February 15-19, 2014, David R. Kaeli and Tipp Moseley (Eds.). ACM, 165. Lukas Stadler, Thomas W\u00fcrthinger, and Hanspeter M\u00f6ssenb\u00f6ck. 2014. Partial Escape Analysis and Scalar Replacement for Java. In 12th Annual IEEE\/ACM International Symposium on Code Generation and Optimization, CGO 2014, Orlando, FL, USA, February 15-19, 2014, David R. Kaeli and Tipp Moseley (Eds.). ACM, 165."},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.5555\/3049832.3049841"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/2584665"},{"key":"e_1_2_1_70_1","volume-title":"Revisited. In SIGMOD Conference. ACM, 307\u2013322","author":"Tahboub Ruby Y.","year":"2018","unstructured":"Ruby Y. Tahboub , Gr\u00e9gory M. Essertel , and Tiark Rompf . 2018 . How to Architect a Query Compiler , Revisited. In SIGMOD Conference. ACM, 307\u2013322 . Ruby Y. Tahboub, Gr\u00e9gory M. Essertel, and Tiark Rompf. 2018. How to Architect a Query Compiler, Revisited. In SIGMOD Conference. ACM, 307\u2013322."},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480915"},{"key":"e_1_2_1_72_1","unstructured":"Amin Timany Robbert Krebbers Derek Dreyer and Lars Birkedal. 2022. A Logical Approach to Type Soundness. https:\/\/iris-project.org\/pdfs\/2022-submitted-logical-type-soundness.pdf Amin Timany Robbert Krebbers Derek Dreyer and Lars Birkedal. 2022. A Logical Approach to Type Soundness. https:\/\/iris-project.org\/pdfs\/2022-submitted-logical-type-soundness.pdf"},{"key":"e_1_2_1_73_1","unstructured":"Ben L. Titzer. 2015. Digging into the TurboFan JIT. http:\/\/web.archive.org\/web\/20220414155345\/https:\/\/v8.dev\/blog\/turbofan-jit Ben L. Titzer. 2015. Digging into the TurboFan JIT. http:\/\/web.archive.org\/web\/20220414155345\/https:\/\/v8.dev\/blog\/turbofan-jit"},{"key":"e_1_2_1_74_1","unstructured":"TPC. 1999. TPC Benchmark H. http:\/\/web.archive.org\/web\/20220407033028\/https:\/\/www.tpc.org\/tpch\/ TPC. 1999. TPC Benchmark H. http:\/\/web.archive.org\/web\/20220407033028\/https:\/\/www.tpc.org\/tpch\/"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.4380090105"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289425"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","DOI":"10.1109\/BigData47090.2019.9006180"},{"key":"e_1_2_1_79_1","volume-title":"Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems","author":"Wang Fei","year":"2018","unstructured":"Fei Wang , James M. Decker , Xilun Wu , Gr\u00e9gory M. Essertel , and Tiark Rompf . 2018. Backpropagation with Callbacks: Foundations for Efficient and Expressive Differentiable Programming . In Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018 , NeurIPS 2018, December 3-8, 2018, Montr\u00e9al, Canada, Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicol\u00f2 Cesa-Bianchi, and Roman Garnett (Eds .). 10201\u201310212. Fei Wang, James M. Decker, Xilun Wu, Gr\u00e9gory M. Essertel, and Tiark Rompf. 2018. Backpropagation with Callbacks: Foundations for Efficient and Expressive Differentiable Programming. In Advances in Neural Information Processing Systems 31: Annual Conference on Neural Information Processing Systems 2018, NeurIPS 2018, December 3-8, 2018, Montr\u00e9al, Canada, Samy Bengio, Hanna M. Wallach, Hugo Larochelle, Kristen Grauman, Nicol\u00f2 Cesa-Bianchi, and Roman Garnett (Eds.). 10201\u201310212."},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341700"},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159876.1159877"},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428232"},{"key":"e_1_2_1_83_1","unstructured":"Guannan Wei Oliver Bra\u010devac Songlin Jia Yuyan Bao and Tiark Rompf. 2023. Polymorphic Reachability Types: Tracking Freshness Aliasing and Separation in Higher-Order Generic Programs. arxiv:2307.13844. Guannan Wei Oliver Bra\u010devac Songlin Jia Yuyan Bao and Tiark Rompf. 2023. Polymorphic Reachability Types: Tracking Freshness Aliasing and Separation in Higher-Order Generic Programs. arxiv:2307.13844."},{"key":"e_1_2_1_84_1","volume-title":"Compiling Parallel Symbolic Execution with Continuations","author":"Wei Guannan","unstructured":"Guannan Wei , Songlin Jia , Ruiqi Gao , Haotian Deng , Shangyin Tan , Oliver Bra\u010devac , and Tiark Rompf . 2023. Compiling Parallel Symbolic Execution with Continuations . In ICSE. IEEE , 1316\u20131328. Guannan Wei, Songlin Jia, Ruiqi Gao, Haotian Deng, Shangyin Tan, Oliver Bra\u010devac, and Tiark Rompf. 2023. Compiling Parallel Symbolic Execution with Continuations. In ICSE. IEEE, 1316\u20131328."},{"key":"e_1_2_1_85_1","doi-asserted-by":"crossref","unstructured":"Guannan Wei Shangyin Tan Oliver Bra\u010devac and Tiark Rompf. 2021. LLSC: a parallel symbolic execution compiler for LLVM IR. In ESEC\/SIGSOFT FSE. ACM 1495\u20131499. Guannan Wei Shangyin Tan Oliver Bra\u010devac and Tiark Rompf. 2021. LLSC: a parallel symbolic execution compiler for LLVM IR. In ESEC\/SIGSOFT FSE. ACM 1495\u20131499.","DOI":"10.1145\/3468264.3473108"},{"key":"e_1_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434304"},{"key":"e_1_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509578.2509581"},{"key":"e_1_2_1_88_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-014-9103-9"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622813","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3622813","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:04Z","timestamp":1750178224000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622813"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,16]]},"references-count":84,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2023,10,16]]}},"alternative-id":["10.1145\/3622813"],"URL":"https:\/\/doi.org\/10.1145\/3622813","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,10,16]]},"assertion":[{"value":"2023-10-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}