A Verified Compiler for a Functional Tensor Language
summary
A mechanically verified implementation of a lowering algorithm for ATL proves that a functional tensor program lowers to imperative loop nests that write exactly the intended tensor values, making this the first verified compiler that separates compute order from storage order via reshape operators. Verification uncovers a soundness bug in the original handling of truncate; the fix is a new static pad type system that enforces truncated entries are padding. Prototype compiles a suite of realistic kernels, preserves prior performance claims (comparable to Halide), and ships artifacts and proofs.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 2:26High-level tensor compilation
- 3:50ATL and trusted lowering
- 4:53Lowering verification concerns
- 6:16Reshape and storage reordering
- 9:03Lowering algorithm correctness
- 11:07Truncation safety issues
- 13:12Padding and truncation safety
- 14:57Pad type checking
- 15:40Compiler evaluation
- 16:24Q&A
related talks
24mVerified Tensor-Program Optimization Via High-Level Scheduling Rewrites
20mA Mechanized Algebra of Verified Data Structures for Optimizing Sparse Tensor Programs
16mTowards formally secure compilation of verified F* programs against unverified ML(…)
33mTeIL: a type-safe imperative Tensor Intermediate Language
20mCompiling Structured Tensor Algebra
20mTensorRight: Automated Verification of Tensor Graph Rewrites
29mTowards Formally Verified Just-In-Time Compilation
21mVerified VCG and Verified Compiler for Dafny