{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:49:45Z","timestamp":1770281385308,"version":"3.49.0"},"reference-count":21,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T00:00:00Z","timestamp":1718841600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["CCF-1846502"],"award-info":[{"award-number":["CCF-1846502"]}],"id":[{"id":"10.13039\/100000001","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":[[2024,6,20]]},"abstract":"<jats:p>\n            Producing efficient array code is crucial in high-performance domains like image processing and machine learning. It requires the ability to control factors like compute intensity and locality by reordering computations into different stages and granularities with respect to where they are stored. However, traditional pure, functional tensor languages struggle to do so. In a previous publication, we introduced ATL as a pure, functional tensor language capable of systematically decoupling compute and storage order via a set of high-level combinators known as reshape operators. Reshape operators are a unique functional-programming construct since they manipulate storage location in the generated code by modifying the indices that appear on the left-hand sides of storage expressions. We present a formal correctness proof for an implementation of the compilation algorithm, marking the first verification of a lowering algorithm targeting imperative loop nests from a source functional language that enables separate control of compute and storage ordering. One of the core difficulties of this proof required properly formulating the complex invariants to ensure that these storage-index remappings were well-formed. Notably, this exercise revealed a\n            <jats:italic toggle=\"yes\">soundness bug<\/jats:italic>\n            in the original published compilation algorithm regarding the truncation reshape operators. Our fix is a new type system that captures safety conditions that were previously implicit and enables us to prove compiler correctness for well-typed source programs. We evaluate this type system and compiler implementation on a range of common programs and optimizations, including but not limited to those previously studied to demonstrate performance comparable to established compilers like Halide.\n          <\/jats:p>","DOI":"10.1145\/3656390","type":"journal-article","created":{"date-parts":[[2024,6,20]],"date-time":"2024-06-20T16:27:20Z","timestamp":1718900840000},"page":"320-342","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["A Verified Compiler for a Functional Tensor Language"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5549-9177","authenticated-orcid":false,"given":"Amanda","family":"Liu","sequence":"first","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3016-1169","authenticated-orcid":false,"given":"Gilbert","family":"Bernstein","sequence":"additional","affiliation":[{"name":"University of Washington, Seattle, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7085-9417","authenticated-orcid":false,"given":"Adam","family":"Chlipala","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6243-9543","authenticated-orcid":false,"given":"Jonathan","family":"Ragan-Kelley","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, USA"}]}],"member":"320","published-online":{"date-parts":[[2024,6,20]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","unstructured":"Oskar Abrahamsson Son Ho Hrutvik Kanabar Ramana Kumar Magnus O. Myreen Michael Norrish and Yong Kiam Tan. 2020. Proof-Producing Synthesis of CakeML from Monadic HOL Functions. 7. Autom. Reason. 64 7 (oct 2020) 1287-1306. https:\/\/doi.org\/10.1007\/s10817-020-09559-8 10.1007\/s10817-020-09559-8","DOI":"10.1007\/s10817-020-09559-8"},{"key":"e_1_3_2_3_1","first-page":"579","article-title":"TVM: An Automated End-toend Optimizing Compiler for Deep Learning.","author":"Chen Tianqi","year":"2018","unstructured":"Tianqi Chen, Thierry Moreau, Ziheng Jiang, Lianmin Zheng, Eddie Yan, Meghan Cowan, Haichen Shen, Leyuan Wang, Yuwei Hu, Luis Ceze, Carlos Guestrin, and Arvind Krishnamurthy. 2018. TVM: An Automated End-toend Optimizing Compiler for Deep Learning. In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (Carlsbad, CA, USA) (OSDI\u201918). USENIX Association, Berkeley, CA, USA, 579-594. http:\/\/dl.acm.org\/citation.cfm?id=3291168.3291211","journal-title":"In Proceedings of the 12th USENIX Conference on Operating Systems Design and Implementation (Carlsbad, CA, USA) (OSDI\u201918)"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527328"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434321"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677006"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/sp.2019.00005"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591268"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_9"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","unstructured":"Peter Lammich. 2019. Refinement to Imperative HOL. 7. Autom. Reason. 62 4 (apr 2019) 481-503. https:\/\/doi.org\/10.1007\/s10817-017-9437-1 10.1007\/s10817-017-9437-1","DOI":"10.1007\/s10817-017-9437-1"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3520306.3534502"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.10932109"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498717"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3587216.3587218"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2364527.2364545"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","unstructured":"Zoe Paraskevopoulou John M. Li and Andrew W. Appel. 2021. Compositional Optimizations for CertiCoq. Proc. ACM Program. Lang. 5 ICFP Article 86 (aug 2021) 30 pages. https:\/\/doi.org\/10.1145\/3473591 10.1145\/3473591","DOI":"10.1145\/3473591"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523706"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51054-1_7"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","unstructured":"Jonathan Ragan-Kelley Connelly Barnes Andrew Adams Sylvain Paris Fr\u00e9do Durand and Saman Amarasinghe 2013. Halide: A Language and Compiler for Optimizing Parallelism Locality and Recomputation in Image Processing Pipelines. SIGPLAN Not. 48 6 (jun 2013) 519-530. https:\/\/doi.org\/10.1145\/2499370.2462176 10.1145\/2499370.2462176","DOI":"10.1145\/2499370.2462176"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3122948.3122949"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656390","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3656390","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:39:51Z","timestamp":1751661591000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3656390"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,20]]},"references-count":21,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2024,6,20]]}},"alternative-id":["10.1145\/3656390"],"URL":"https:\/\/doi.org\/10.1145\/3656390","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,20]]},"assertion":[{"value":"2024-06-20","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}