A Verified Compiler for a Functional Tensor Language - PLDI 2024

Explore a groundbreaking video presentation from PLDI 2024 that delves into the development of a verified compiler for a functional tensor language. Discover how researchers from MIT and the University of Washington tackle the challenge of producing efficient array code for high-performance domains like image processing and machine learning. Learn about ATL, a pure functional tensor language that introduces reshape operators to decouple compute and storage order. Understand the complexities involved in formally proving the correctness of the compilation algorithm, including the discovery and resolution of a soundness bug in the original published algorithm. Examine the new type system developed to capture safety conditions and enable compiler correctness proofs for well-typed source programs. Gain insights into the evaluation of this type system and compiler implementation across various programs and optimizations, demonstrating performance comparable to established compilers like Halide.