{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:43:49Z","timestamp":1780994629574,"version":"3.54.1"},"reference-count":71,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","license":[{"start":{"date-parts":[[2019,10,10]],"date-time":"2019-10-10T00:00:00Z","timestamp":1570665600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100016682","name":"VMware","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100016682","id-type":"DOI","asserted-by":"crossref"}]},{"name":"Facebook"},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1553471, 1564207, 1918483"],"award-info":[{"award-number":["1553471, 1564207, 1918483"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000015","name":"U.S. Department of Energy","doi-asserted-by":"publisher","award":["DE-SC001805"],"award-info":[{"award-number":["DE-SC001805"]}],"id":[{"id":"10.13039\/100000015","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100006785","name":"Google","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100006785","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,10,10]]},"abstract":"<jats:p>Despite decades of progress, static analysis tools still have great difficulty dealing with programs that combine arithmetic, loops, dynamic memory allocation, and linked data structures. In this paper we draw attention to two fundamental reasons for this difficulty: First, typical underlying program abstractions are low-level and inherently scalar, characterizing compound entities like data structures or results computed through iteration only indirectly. Second, to ensure termination, analyses typically project away the dimension of time, and merge information per program point, which incurs a loss in precision.<\/jats:p>\n          <jats:p>As a remedy, we propose to make collective operations first-class in program analysis \u2013 inspired by \u03a3-notation in mathematics, and also by the success of high-level intermediate languages based on @map\/reduce@ operations in program generators and aggressive optimizing compilers for domain-specific languages (DSLs). We further propose a novel structured heap abstraction that preserves a symbolic dimension of time, reflecting the program\u2019s loop structure and thus unambiguously correlating multiple temporal points in the dynamic execution with a single point in the program text.<\/jats:p>\n          <jats:p>This paper presents a formal model, based on a high-level intermediate analysis language, a practical realization in a prototype tool that analyzes C code, and an experimental evaluation that demonstrates competitive results on a series of benchmarks. Remarkably, our implementation achieves these results in a fully semantics-preserving strongest-postcondition model, which is a worst-case for analysis\/verification. The underlying ideas, however, are not tied to this model and would equally apply in other settings, e.g., demand-driven invariant inference in a weakest-precondition model. Given its semantics-preserving nature, our implementation is not limited to analysis for verification, but can also check program equivalence, and translate legacy C code to high-performance DSLs.<\/jats:p>","DOI":"10.1145\/3360583","type":"journal-article","created":{"date-parts":[[2019,10,11]],"date-time":"2019-10-11T14:53:33Z","timestamp":1570805613000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Precise reasoning with structured time, structured heaps, and collective operations"],"prefix":"10.1145","volume":"3","author":[{"given":"Gr\u00e9gory M.","family":"Essertel","sequence":"first","affiliation":[{"name":"Purdue University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Guannan","family":"Wei","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tiark","family":"Rompf","sequence":"additional","affiliation":[{"name":"Purdue University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,10,10]]},"reference":[{"key":"e_1_2_2_1_1","first-page":"67","article-title":"Leveraging Parallel Data Processing Frameworks with Verified Lifting","volume":"229","author":"Safeer Ahmad Maaz Bin","year":"2016","unstructured":"Maaz Bin Safeer Ahmad and Alvin Cheung . 2016 . Leveraging Parallel Data Processing Frameworks with Verified Lifting . In SYNT\/CAV (EPTCS) , Vol. 229. 67 \u2013 83 . Maaz Bin Safeer Ahmad and Alvin Cheung. 2016. Leveraging Parallel Data Processing Frameworks with Verified Lifting. In SYNT\/CAV (EPTCS), Vol. 229. 67\u201383.","journal-title":"SYNT\/CAV (EPTCS)"},{"key":"e_1_2_2_2_1","doi-asserted-by":"crossref","unstructured":"Nada Amin and Tiark Rompf. 2017. Type soundness proofs with definitional interpreters. In POPL. ACM 666\u2013679.  Nada Amin and Tiark Rompf. 2017. Type soundness proofs with definitional interpreters. In POPL. ACM 666\u2013679.","DOI":"10.1145\/3093333.3009866"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/278283.278285"},{"key":"e_1_2_2_4_1","volume-title":"Zima","author":"Bachmann Olaf","year":"1994","unstructured":"Olaf Bachmann , Paul S. Wang , and Eugene V . Zima . 1994 . Chains of Recurrences - a Method to Expedite the Evaluation of Closed-form Functions. In ISSAC. ACM , 242\u2013249. Olaf Bachmann, Paul S. Wang, and Eugene V. Zima. 1994. Chains of Recurrences - a Method to Expedite the Evaluation of Closed-form Functions. In ISSAC. ACM, 242\u2013249."},{"key":"e_1_2_2_5_1","volume-title":"PENCIL: A Platform-Neutral Compute Intermediate Language for Accelerator Programming","author":"Baghdadi Riyadh","year":"2015","unstructured":"Riyadh Baghdadi , Ulysse Beaugnon , Albert Cohen , Tobias Grosser , Michael Kruse , Chandan Reddy , Sven Verdoolaege , Adam Betts , Alastair F. Donaldson , Jeroen Ketema , Javed Absar , Sven van Haastregt , Alexey Kravets , Anton Lokhmotov , Robert David , and Elnar Hajiyev . 2015 . PENCIL: A Platform-Neutral Compute Intermediate Language for Accelerator Programming . In PACT. IEEE Computer Society , 138\u2013149. Riyadh Baghdadi, Ulysse Beaugnon, Albert Cohen, Tobias Grosser, Michael Kruse, Chandan Reddy, Sven Verdoolaege, Adam Betts, Alastair F. Donaldson, Jeroen Ketema, Javed Absar, Sven van Haastregt, Alexey Kravets, Anton Lokhmotov, Robert David, and Elnar Hajiyev. 2015. PENCIL: A Platform-Neutral Compute Intermediate Language for Accelerator Programming. In PACT. IEEE Computer Society, 138\u2013149."},{"key":"e_1_2_2_6_1","volume-title":"CC (Lecture Notes in Computer Science)","author":"Benabderrahmane Mohamed-Walid","unstructured":"Mohamed-Walid Benabderrahmane , Louis-No\u00ebl Pouchet , Albert Cohen , and C\u00e9dric Bastoul . 2010. The Polyhedral Model Is More Widely Applicable Than You Think . In CC (Lecture Notes in Computer Science) , Vol. 6011 . Springer , 283\u2013303. Mohamed-Walid Benabderrahmane, Louis-No\u00ebl Pouchet, Albert Cohen, and C\u00e9dric Bastoul. 2010. The Polyhedral Model Is More Widely Applicable Than You Think. In CC (Lecture Notes in Computer Science), Vol. 6011. Springer, 283\u2013303."},{"key":"e_1_2_2_7_1","volume-title":"ESOP (Lecture Notes in Computer Science)","author":"Bergstra Jan A.","unstructured":"Jan A. Bergstra , T. B. Dinesh , John Field , and Jan Heering . 1996. A Complete Transformational Toolkit for Compilers . In ESOP (Lecture Notes in Computer Science) , Vol. 1058 . Springer , 92\u2013107. Jan A. Bergstra, T. B. Dinesh, John Field, and Jan Heering. 1996. A Complete Transformational Toolkit for Compilers. In ESOP (Lecture Notes in Computer Science), Vol. 1058. Springer, 92\u2013107."},{"key":"e_1_2_2_8_1","volume-title":"TACAS (Lecture Notes in Computer Science)","author":"Beyer Dirk","unstructured":"Dirk Beyer . 2012. Competition on Software Verification - (SV-COMP) . In TACAS (Lecture Notes in Computer Science) , Vol. 7214 . Springer , 504\u2013524. Dirk Beyer. 2012. Competition on Software Verification - (SV-COMP). In TACAS (Lecture Notes in Computer Science), Vol. 7214. Springer, 504\u2013524."},{"key":"e_1_2_2_9_1","volume-title":"CAV (Lecture Notes in Computer Science)","author":"Beyer Dirk","unstructured":"Dirk Beyer and M. Erkan Keremoglu . 2011. CPAchecker: A Tool for Configurable Software Verification . In CAV (Lecture Notes in Computer Science) , Vol. 6806 . Springer , 184\u2013190. Dirk Beyer and M. Erkan Keremoglu. 2011. CPAchecker: A Tool for Configurable Software Verification. In CAV (Lecture Notes in Computer Science), Vol. 6806. Springer, 184\u2013190."},{"key":"e_1_2_2_10_1","volume-title":"Bingham and Zvonimir Rakamaric","author":"Jesse","year":"2006","unstructured":"Jesse D. Bingham and Zvonimir Rakamaric . 2006 . A Logic and Decision Procedure for Predicate Abstraction of HeapManipulating Programs. In VMCAI (Lecture Notes in Computer Science), Vol. 3855 . Springer , 207\u2013221. Jesse D. Bingham and Zvonimir Rakamaric. 2006. A Logic and Decision Procedure for Predicate Abstraction of HeapManipulating Programs. In VMCAI (Lecture Notes in Computer Science), Vol. 3855. Springer, 207\u2013221."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2984450.2984457"},{"key":"e_1_2_2_12_1","volume-title":"Christopher R. Aberger, and Kunle Olukotun.","author":"Brown Kevin J.","year":"2016","unstructured":"Kevin J. Brown , HyoukJoong Lee , Tiark Rompf , Arvind K. Sujeeth , Christopher De Sa , Christopher R. Aberger, and Kunle Olukotun. 2016 . Have abstraction and eat performance, too: optimized heterogeneous computing with parallel patterns. In CGO. ACM , 194\u2013205. Kevin J. Brown, HyoukJoong Lee, Tiark Rompf, Arvind K. Sujeeth, Christopher De Sa, Christopher R. Aberger, and Kunle Olukotun. 2016. Have abstraction and eat performance, too: optimized heterogeneous computing with parallel patterns. In CGO. ACM, 194\u2013205."},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/PACT.2011.15"},{"key":"e_1_2_2_14_1","volume-title":"NFM (Lecture Notes in Computer Science)","author":"Calcagno Cristiano","unstructured":"Cristiano Calcagno , Dino Distefano , J\u00e9r\u00e9my Dubreil , Dominik Gabi , Pieter Hooimeijer , Martino Luca , Peter W. O\u2019Hearn , Irene Papakonstantinou , Jim Purbrick , and Dulma Rodriguez . 2015. Moving Fast with Software Verification . In NFM (Lecture Notes in Computer Science) , Vol. 9058 . Springer , 3\u201311. Cristiano Calcagno, Dino Distefano, J\u00e9r\u00e9my Dubreil, Dominik Gabi, Pieter Hooimeijer, Martino Luca, Peter W. O\u2019Hearn, Irene Papakonstantinou, Jim Purbrick, and Dulma Rodriguez. 2015. Moving Fast with Software Verification. In NFM (Lecture Notes in Computer Science), Vol. 9058. Springer, 3\u201311."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049697.2049700"},{"key":"e_1_2_2_16_1","doi-asserted-by":"crossref","unstructured":"Manuel M. T. Chakravarty Gabriele Keller Sean Lee Trevor L. McDonell and Vinod Grover. 2011. Accelerating Haskell array codes with multicore GP Us. In DAMP. ACM 3\u201314.  Manuel M. T. Chakravarty Gabriele Keller Sean Lee Trevor L. McDonell and Vinod Grover. 2011. Accelerating Haskell array codes with multicore GP Us. In DAMP. ACM 3\u201314.","DOI":"10.1145\/1926354.1926358"},{"key":"e_1_2_2_17_1","volume-title":"A Discipline of Programming","author":"Dijkstra Edsger Wybe","unstructured":"Edsger Wybe Dijkstra . 1976. A Discipline of Programming ( 1 st ed.). Prentice Hall PTR , Upper Saddle River, NJ, USA. Edsger Wybe Dijkstra. 1976. A Discipline of Programming (1st ed.). Prentice Hall PTR, Upper Saddle River, NJ, USA.","edition":"1"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-011-0127-z"},{"key":"e_1_2_2_19_1","doi-asserted-by":"crossref","unstructured":"Isil Dillig Thomas Dillig and Alex Aiken. 2011b. Precise reasoning for programs using containers. In POPL. ACM 187\u2013200.  Isil Dillig Thomas Dillig and Alex Aiken. 2011b. Precise reasoning for programs using containers. In POPL. ACM 187\u2013200.","DOI":"10.1145\/1925844.1926407"},{"key":"e_1_2_2_20_1","volume-title":"TACAS (Lecture Notes in Computer Science)","author":"Distefano Dino","unstructured":"Dino Distefano , Peter W. O\u2019Hearn , and Hongseok Yang . 2006. A Local Shape Analysis Based on Separation Logic . In TACAS (Lecture Notes in Computer Science) , Vol. 3920 . Springer , 287\u2013302. Dino Distefano, Peter W. O\u2019Hearn, and Hongseok Yang. 2006. A Local Shape Analysis Based on Separation Logic. In TACAS (Lecture Notes in Computer Science), Vol. 3920. Springer, 287\u2013302."},{"key":"e_1_2_2_21_1","volume-title":"Gallivan","author":"Van Engelen Robert A.","year":"2004","unstructured":"Robert A. Van Engelen , Johnnie Birch , Yixin Shou , Burt Walsh , and Kyle A . Gallivan . 2004 . A unified framework for nonlinear dependence testing and symbolic analysis. In ICS. ACM , 106\u2013115. Robert A. Van Engelen, Johnnie Birch, Yixin Shou, Burt Walsh, and Kyle A. Gallivan. 2004. A unified framework for nonlinear dependence testing and symbolic analysis. In ICS. ACM, 106\u2013115."},{"key":"e_1_2_2_22_1","volume-title":"Compositional Recurrence Analysis","author":"Farzan Azadeh","unstructured":"Azadeh Farzan and Zachary Kincaid . 2015. Compositional Recurrence Analysis . In FMCAD. IEEE , 57\u201364. Azadeh Farzan and Zachary Kincaid. 2015. Compositional Recurrence Analysis. In FMCAD. IEEE, 57\u201364."},{"key":"e_1_2_2_23_1","volume-title":"April 1820","author":"Fourier Joseph","year":"1820","unstructured":"Joseph Fourier . 1820. Extrait d\u2019une m\u00e9moire sur le refroidissement s\u00e9culaire du globe terrestre. Bulletin des Sciences par la Soci\u00e9t\u00e9 Philomathique de Paris , April 1820 ( 1820 ), 58\u201370. Joseph Fourier. 1820. Extrait d\u2019une m\u00e9moire sur le refroidissement s\u00e9culaire du globe terrestre. Bulletin des Sciences par la Soci\u00e9t\u00e9 Philomathique de Paris, April 1820 (1820), 58\u201370."},{"key":"e_1_2_2_24_1","doi-asserted-by":"crossref","unstructured":"Denis Gopan Thomas W. Reps and Shmuel Sagiv. 2005. A framework for numeric analysis of array operations. In POPL. ACM 338\u2013350.  Denis Gopan Thomas W. Reps and Shmuel Sagiv. 2005. A framework for numeric analysis of array operations. In POPL. ACM 338\u2013350.","DOI":"10.1145\/1047659.1040333"},{"key":"e_1_2_2_25_1","volume-title":"Navas","author":"Gurfinkel Arie","year":"2015","unstructured":"Arie Gurfinkel , Temesghen Kahsai , Anvesh Komuravelli , and Jorge A . Navas . 2015 . The SeaHorn Verification Framework. In CAV (1) (Lecture Notes in Computer Science), Vol. 9206 . Springer , 343\u2013361. Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli, and Jorge A. Navas. 2015. The SeaHorn Verification Framework. In CAV (1) (Lecture Notes in Computer Science), Vol. 9206. Springer, 343\u2013361."},{"key":"e_1_2_2_26_1","volume-title":"LPAR (Yogyakarta) (Lecture Notes in Computer Science)","author":"Henzinger Thomas A.","unstructured":"Thomas A. Henzinger , Thibaud Hottelier , Laura Kov\u00e1cs , and Andrey Rybalchenko . 2010. Aligators for Arrays (Tool Paper) . In LPAR (Yogyakarta) (Lecture Notes in Computer Science) , Vol. 6397 . Springer , 348\u2013356. Thomas A. Henzinger, Thibaud Hottelier, Laura Kov\u00e1cs, and Andrey Rybalchenko. 2010. Aligators for Arrays (Tool Paper). In LPAR (Yogyakarta) (Lecture Notes in Computer Science), Vol. 6397. Springer, 348\u2013356."},{"key":"e_1_2_2_27_1","doi-asserted-by":"crossref","unstructured":"David Van Horn and Matthew Might. 2010. Abstracting abstract machines. In ICFP. ACM 51\u201362.  David Van Horn and Matthew Might. 2010. Abstracting abstract machines. In ICFP. ACM 51\u201362.","DOI":"10.1145\/1932681.1863553"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/358896.358899"},{"key":"e_1_2_2_29_1","doi-asserted-by":"crossref","unstructured":"Bertrand Jeannet Peter Schrammel and Sriram Sankaranarayanan. 2014. Abstract acceleration of general linear loops. In POPL. ACM 529\u2013540.  Bertrand Jeannet Peter Schrammel and Sriram Sankaranarayanan. 2014. Abstract acceleration of general linear loops. In POPL. ACM 529\u2013540.","DOI":"10.1145\/2578855.2535843"},{"key":"e_1_2_2_30_1","doi-asserted-by":"crossref","unstructured":"Shoaib Kamil Alvin Cheung Shachar Itzhaky and Armando Solar-Lezama. 2016. Verified lifting of stencil computations. In PLDI. ACM 711\u2013726.  Shoaib Kamil Alvin Cheung Shachar Itzhaky and Armando Solar-Lezama. 2016. Verified lifting of stencil computations. In PLDI. ACM 711\u2013726.","DOI":"10.1145\/2980983.2908117"},{"key":"e_1_2_2_31_1","volume-title":"Ashkan Forouhi Boroujeni, and Thomas Reps","author":"Kincaid Zachary","year":"2017","unstructured":"Zachary Kincaid , Jason Breck , Ashkan Forouhi Boroujeni, and Thomas Reps . 2017 . Compositional Recurrence Analysis Revisited. In PLDI. Zachary Kincaid, Jason Breck, Ashkan Forouhi Boroujeni, and Thomas Reps. 2017. Compositional Recurrence Analysis Revisited. In PLDI."},{"key":"e_1_2_2_32_1","doi-asserted-by":"crossref","unstructured":"Kathleen Knobe and Vivek Sarkar. 1998. Array SSA Form and Its Use in Parallelization. In POPL. ACM 107\u2013120.  Kathleen Knobe and Vivek Sarkar. 1998. Array SSA Form and Its Use in Parallelization. In POPL. ACM 107\u2013120.","DOI":"10.1145\/268946.268956"},{"key":"e_1_2_2_33_1","volume-title":"TACAS (Lecture Notes in Computer Science)","author":"Kov\u00e1cs Laura","unstructured":"Laura Kov\u00e1cs . 2008. Reasoning Algebraically About P-Solvable Loops . In TACAS (Lecture Notes in Computer Science) , Vol. 4963 . Springer , 249\u2013264. Laura Kov\u00e1cs. 2008. Reasoning Algebraically About P-Solvable Loops. In TACAS (Lecture Notes in Computer Science), Vol. 4963. Springer, 249\u2013264."},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/MM.2011.68"},{"key":"e_1_2_2_35_1","doi-asserted-by":"crossref","unstructured":"Sorin Lerner David Grove and Craig Chambers. 2002. Composing dataflow analyses and transformations. In POPL. ACM 270\u2013282.  Sorin Lerner David Grove and Craig Chambers. 2002. Composing dataflow analyses and transformations. In POPL. ACM 270\u2013282.","DOI":"10.1145\/565816.503298"},{"key":"e_1_2_2_36_1","doi-asserted-by":"crossref","unstructured":"Sorin Lerner Todd D. Millstein and Craig Chambers. 2003. Automatically proving the correctness of compiler optimizations. In PLDI. 220\u2013231.  Sorin Lerner Todd D. Millstein and Craig Chambers. 2003. Automatically proving the correctness of compiler optimizations. In PLDI. 220\u2013231.","DOI":"10.1145\/780822.781156"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2990195"},{"key":"e_1_2_2_38_1","volume-title":"Newton","author":"McDonell Trevor L.","year":"2015","unstructured":"Trevor L. McDonell , Manuel M. T. Chakravarty , Vinod Grover , and Ryan R . Newton . 2015 . Type-safe runtime code generation: accelerate to LLVM. In Haskell. ACM , 201\u2013212. Trevor L. McDonell, Manuel M. T. Chakravarty, Vinod Grover, and Ryan R. Newton. 2015. Type-safe runtime code generation: accelerate to LLVM. In Haskell. ACM, 201\u2013212."},{"key":"e_1_2_2_39_1","volume-title":"Amarasinghe","author":"Mendis Charith","year":"2015","unstructured":"Charith Mendis , Jeffrey Bosboom , Kevin Wu , Shoaib Kamil , Jonathan Ragan-Kelley , Sylvain Paris , Qin Zhao , and Saman P . Amarasinghe . 2015 . Helium: lifting high-performance stencil kernels from stripped x86 binaries to Halide DSL code. In PLDI. ACM , 391\u2013402. Charith Mendis, Jeffrey Bosboom, Kevin Wu, Shoaib Kamil, Jonathan Ragan-Kelley, Sylvain Paris, Qin Zhao, and Saman P. Amarasinghe. 2015. Helium: lifting high-performance stencil kernels from stripped x86 binaries to Halide DSL code. In PLDI. ACM, 391\u2013402."},{"key":"e_1_2_2_40_1","doi-asserted-by":"crossref","unstructured":"Hakjoo Oh Kihong Heo Wonchan Lee Woosuk Lee and Kwangkeun Yi. 2012. Design and implementation of sparse global analyses for C-like languages. In PLDI. ACM 229\u2013238.  Hakjoo Oh Kihong Heo Wonchan Lee Woosuk Lee and Kwangkeun Yi. 2012. Design and implementation of sparse global analyses for C-like languages. In PLDI. ACM 229\u2013238.","DOI":"10.1145\/2345156.2254092"},{"key":"e_1_2_2_41_1","volume-title":"ESOP (Lecture Notes in Computer Science)","author":"Owens Scott","unstructured":"Scott Owens , Magnus O. Myreen , Ramana Kumar , and Yong Kiam Tan . 2016. Functional Big-Step Semantics . In ESOP (Lecture Notes in Computer Science) , Vol. 9632 . Springer , 589\u2013615. Scott Owens, Magnus O. Myreen, Ramana Kumar, and Yong Kiam Tan. 2016. Functional Big-Step Semantics. In ESOP (Lecture Notes in Computer Science), Vol. 9632. Springer, 589\u2013615."},{"key":"e_1_2_2_42_1","doi-asserted-by":"crossref","unstructured":"William Pugh. 1991. The Omega test: a fast and practical integer programming algorithm for dependence analysis. In SC. ACM 4\u201313.  William Pugh. 1991. The Omega test: a fast and practical integer programming algorithm for dependence analysis. In SC. ACM 4\u201313.","DOI":"10.1145\/125826.125848"},{"key":"e_1_2_2_43_1","doi-asserted-by":"crossref","unstructured":"Cosmin Radoi Stephen J. Fink Rodric M. Rabbah and Manu Sridharan. 2014. Translating imperative code to MapReduce. In OOPSLA. ACM 909\u2013927.  Cosmin Radoi Stephen J. Fink Rodric M. Rabbah and Manu Sridharan. 2014. Translating imperative code to MapReduce. In OOPSLA. ACM 909\u2013927.","DOI":"10.1145\/2714064.2660228"},{"key":"e_1_2_2_44_1","volume-title":"Amarasinghe","author":"Ragan-Kelley Jonathan","year":"2013","unstructured":"Jonathan Ragan-Kelley , Connelly Barnes , Andrew Adams , Sylvain Paris , Fr\u00e9do Durand , and Saman P . Amarasinghe . 2013 . Halide: a language and compiler for optimizing parallelism, locality, and recomputation in image processing pipelines. In PLDI. ACM , 519\u2013530. Jonathan Ragan-Kelley, Connelly Barnes, Andrew Adams, Sylvain Paris, Fr\u00e9do Durand, and Saman P. Amarasinghe. 2013. Halide: a language and compiler for optimizing parallelism, locality, and recomputation in image processing pipelines. In PLDI. ACM, 519\u2013530."},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/48014.48021"},{"key":"e_1_2_2_46_1","doi-asserted-by":"crossref","unstructured":"Veselin Raychev Madanlal Musuvathi and Todd Mytkowicz. 2015. Parallelizing user-defined aggregations using symbolic execution. In SOSP. ACM 153\u2013167.  Veselin Raychev Madanlal Musuvathi and Todd Mytkowicz. 2015. Parallelizing user-defined aggregations using symbolic execution. In SOSP. ACM 153\u2013167.","DOI":"10.1145\/2815400.2815418"},{"key":"e_1_2_2_47_1","doi-asserted-by":"crossref","unstructured":"Thomas W. Reps Emma Turetsky and Prathmesh Prabhu. 2016. Newtonian program analysis via tensor product. In POPL. ACM 663\u2013677.  Thomas W. Reps Emma Turetsky and Prathmesh Prabhu. 2016. Newtonian program analysis via tensor product. In POPL. ACM 663\u2013677.","DOI":"10.1145\/2914770.2837659"},{"key":"e_1_2_2_48_1","volume-title":"Separation Logic: A Logic for Shared Mutable Data Structures","author":"Reynolds John C.","year":"2002","unstructured":"John C. Reynolds . 2002 . Separation Logic: A Logic for Shared Mutable Data Structures . In LICS. IEEE Computer Society , 55\u201374. John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In LICS. IEEE Computer Society, 55\u201374."},{"key":"e_1_2_2_49_1","volume-title":"Brown","author":"Rompf Tiark","year":"2017","unstructured":"Tiark Rompf and Kevin J . Brown . 2017 . Functional parallels of sequential imperatives (short paper). In PEPM. ACM , 83\u201388. Tiark Rompf and Kevin J. Brown. 2017. Functional parallels of sequential imperatives (short paper). In PEPM. ACM, 83\u201388."},{"key":"e_1_2_2_50_1","doi-asserted-by":"crossref","unstructured":"Tiark Rompf Arvind K. Sujeeth Nada Amin Kevin Brown Vojin Jovanovic HyoukJoong Lee Manohar Jonnalagedda Kunle Olukotun and Martin Odersky. 2013. Optimizing Data Structures in High-Level Programs (POPL).  Tiark Rompf Arvind K. Sujeeth Nada Amin Kevin Brown Vojin Jovanovic HyoukJoong Lee Manohar Jonnalagedda Kunle Olukotun and Martin Odersky. 2013. Optimizing Data Structures in High-Level Programs (POPL).","DOI":"10.1145\/2429069.2429128"},{"key":"e_1_2_2_51_1","doi-asserted-by":"crossref","unstructured":"Tiark Rompf Arvind K. Sujeeth Kevin J. Brown HyoukJoong Lee Hassan Chafi and Kunle Olukotun. 2014. Surgical precision JIT compilers. In PLDI. ACM 41\u201352.  Tiark Rompf Arvind K. Sujeeth Kevin J. Brown HyoukJoong Lee Hassan Chafi and Kunle Olukotun. 2014. Surgical precision JIT compilers. In PLDI. ACM 41\u201352.","DOI":"10.1145\/2666356.2594316"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.66.5"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/514188.514190"},{"key":"e_1_2_2_54_1","first-page":"193","article-title":"Set theory as a language for program specification and programming. Courant Institute of Mathematical Sciences","volume":"12","author":"Schwartz Jack","year":"1970","unstructured":"Jack Schwartz . 1970 . Set theory as a language for program specification and programming. Courant Institute of Mathematical Sciences , New York University 12 (1970), 193 \u2013 208 . Jack Schwartz. 1970. Set theory as a language for program specification and programming. Courant Institute of Mathematical Sciences, New York University 12 (1970), 193\u2013208.","journal-title":"New York University"},{"key":"e_1_2_2_55_1","unstructured":"Jeremy G. Siek. 2016. Denotational Semantics of IMP without the Least Fixed Point. http:\/\/siek.blogspot.ch\/2016\/12\/ denotational-semantics-of-imp-without.html.  Jeremy G. Siek. 2016. Denotational Semantics of IMP without the Least Fixed Point. http:\/\/siek.blogspot.ch\/2016\/12\/ denotational-semantics-of-imp-without.html."},{"key":"e_1_2_2_56_1","volume-title":"Declarative semantics for functional languages: compositional, extensional, and elementary. CoRR abs\/1707.03762","author":"Siek Jeremy G.","year":"2017","unstructured":"Jeremy G. Siek . 2017. Declarative semantics for functional languages: compositional, extensional, and elementary. CoRR abs\/1707.03762 ( 2017 ). arXiv: 1707.03762 http:\/\/arxiv.org\/abs\/1707.03762 Jeremy G. Siek. 2017. Declarative semantics for functional languages: compositional, extensional, and elementary. CoRR abs\/1707.03762 (2017). arXiv: 1707.03762 http:\/\/arxiv.org\/abs\/1707.03762"},{"key":"e_1_2_2_57_1","doi-asserted-by":"crossref","unstructured":"Calvin Smith and Aws Albarghouthi. 2016. MapReduce program synthesis. In PLDI. ACM 326\u2013340.  Calvin Smith and Aws Albarghouthi. 2016. MapReduce program synthesis. In PLDI. ACM 326\u2013340.","DOI":"10.1145\/2980983.2908102"},{"key":"e_1_2_2_58_1","doi-asserted-by":"crossref","unstructured":"Michel Steuwer Christian Fensch Sam Lindley and Christophe Dubach. 2015. Generating performance portable code using rewrite rules: from high-level functional expressions to high-performance OpenCL code. In ICFP. ACM 205\u2013217.  Michel Steuwer Christian Fensch Sam Lindley and Christophe Dubach. 2015. Generating performance portable code using rewrite rules: from high-level functional expressions to high-performance OpenCL code. In ICFP. ACM 205\u2013217.","DOI":"10.1145\/2858949.2784754"},{"key":"e_1_2_2_59_1","doi-asserted-by":"crossref","unstructured":"Michel Steuwer Toomas Remmelg and Christophe Dubach. 2017. Lift: a functional data-parallel IR for high-performance GP U code generation. In CGO. ACM 74\u201385.  Michel Steuwer Toomas Remmelg and Christophe Dubach. 2017. Lift: a functional data-parallel IR for high-performance GP U code generation. In CGO. ACM 74\u201385.","DOI":"10.1109\/CGO.2017.7863730"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/2584665"},{"key":"e_1_2_2_61_1","volume-title":"Proceedings of the 28th International Conference on Machine Learning (ICML).","author":"Sujeeth A. K.","unstructured":"A. K. Sujeeth , H. Lee , K. J. Brown , T. Rompf , Michael Wu , A. R. Atreya , M. Odersky , and K. Olukotun . 2011. OptiML: an Implicitly Parallel Domain-Specific Language for Machine Learning . In Proceedings of the 28th International Conference on Machine Learning (ICML). A. K. Sujeeth, H. Lee, K. J. Brown, T. Rompf, Michael Wu, A. R. Atreya, M. Odersky, and K. Olukotun. 2011. OptiML: an Implicitly Parallel Domain-Specific Language for Machine Learning. In Proceedings of the 28th International Conference on Machine Learning (ICML)."},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/2605685"},{"key":"e_1_2_2_63_1","volume-title":"Newton","author":"Svensson Bo Joel","year":"2015","unstructured":"Bo Joel Svensson , Michael Vollmer , Eric Holk , Trevor L. McDonell , and Ryan R . Newton . 2015 . Converting data-parallelism to task-parallelism by rewrites: purely functional programs across multiple GP Us. In FHPC\/ICFP. ACM , 12\u201322. Bo Joel Svensson, Michael Vollmer, Eric Holk, Trevor L. McDonell, and Ryan R. Newton. 2015. Converting data-parallelism to task-parallelism by rewrites: purely functional programs across multiple GP Us. In FHPC\/ICFP. ACM, 12\u201322."},{"key":"e_1_2_2_64_1","doi-asserted-by":"crossref","unstructured":"Tian Tan Yue Li and Jingling Xue. 2017. Efficient and precise points-to analysis: modeling the heap by merging equivalent automata. In PLDI. ACM 278\u2013291.  Tian Tan Yue Li and Jingling Xue. 2017. Efficient and precise points-to analysis: modeling the heap by merging equivalent automata. In PLDI. ACM 278\u2013291.","DOI":"10.1145\/3140587.3062360"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/322261.322273"},{"key":"e_1_2_2_66_1","doi-asserted-by":"crossref","unstructured":"Ross Tate Michael Stepp and Sorin Lerner. 2010. Generating compiler optimizations from proofs. In POPL. 389\u2013402.  Ross Tate Michael Stepp and Sorin Lerner. 2010. Generating compiler optimizations from proofs. In POPL. 389\u2013402.","DOI":"10.1145\/1707801.1706345"},{"key":"e_1_2_2_67_1","volume-title":"Equality Saturation: A New Approach to Optimization. Logical Methods in Computer Science 7, 1","author":"Tate Ross","year":"2011","unstructured":"Ross Tate , Michael Stepp , Zachary Tatlock , and Sorin Lerner . 2011 . Equality Saturation: A New Approach to Optimization. Logical Methods in Computer Science 7, 1 (2011). Ross Tate, Michael Stepp, Zachary Tatlock, and Sorin Lerner. 2011. Equality Saturation: A New Approach to Optimization. Logical Methods in Computer Science 7, 1 (2011)."},{"key":"e_1_2_2_68_1","volume-title":"Eric Holk, and Ryan R. Newton.","author":"Vollmer Michael","year":"2015","unstructured":"Michael Vollmer , Bo Joel Svensson , Eric Holk, and Ryan R. Newton. 2015 . Meta-programming and auto-tuning in the search for high performance GP U code. In FHPC\/ICFP. ACM , 1\u201311. Michael Vollmer, Bo Joel Svensson, Eric Holk, and Ryan R. Newton. 2015. Meta-programming and auto-tuning in the search for high performance GP U code. In FHPC\/ICFP. ACM, 1\u201311."},{"key":"e_1_2_2_69_1","doi-asserted-by":"crossref","unstructured":"Bin Xin William N. Sumner and Xiangyu Zhang. 2008. Efficient program execution indexing. In PLDI. ACM 238\u2013248.  Bin Xin William N. Sumner and Xiangyu Zhang. 2008. Efficient program execution indexing. In PLDI. ACM 238\u2013248.","DOI":"10.1145\/1379022.1375611"},{"key":"e_1_2_2_70_1","volume-title":"No More Gotos: Decompilation Using Pattern-Independent Control-Flow Structuring and Semantic-Preserving Transformations","author":"Yakdan Khaled","unstructured":"Khaled Yakdan , Sebastian Eschweiler , Elmar Gerhards-Padilla , and Matthew Smith . 2015. No More Gotos: Decompilation Using Pattern-Independent Control-Flow Structuring and Semantic-Preserving Transformations . In NDSS. The Internet Society . Khaled Yakdan, Sebastian Eschweiler, Elmar Gerhards-Padilla, and Matthew Smith. 2015. No More Gotos: Decompilation Using Pattern-Independent Control-Flow Structuring and Semantic-Preserving Transformations. In NDSS. The Internet Society."},{"key":"e_1_2_2_71_1","doi-asserted-by":"crossref","unstructured":"He Zhu Stephen Magill and Suresh Jagannathan. 2018. A data-driven CHC solver. In PLDI. ACM 707\u2013721.  He Zhu Stephen Magill and Suresh Jagannathan. 2018. A data-driven CHC solver. In PLDI. ACM 707\u2013721.","DOI":"10.1145\/3296979.3192416"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360583","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360583","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3360583","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:22:59Z","timestamp":1750202579000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3360583"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,10,10]]},"references-count":71,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2019,10,10]]}},"alternative-id":["10.1145\/3360583"],"URL":"https:\/\/doi.org\/10.1145\/3360583","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,10,10]]},"assertion":[{"value":"2019-10-10","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}