Mechanical Proofs in an Array-Combinator Language
summary
Prototype system converts functional data parallel programs into index functions that map indices to values and generates algebraic queries proving properties like permutation, no duplicates, and bounds. It uses a custom, still-naive algebraic solver over sums-of-products expressions and range environments, performs case splitting and recurrence substitution, and successfully proves partitioning examples so optimizations such as skipping destination initialization for scatter become sound. Work in progress but prototype produces and displays intermediate index functions for verification.
AI-written summary · about
chapters (13)
- 0:00Mechanical proofs in Fuar
- 1:50Prove array properties in Fuar
- 4:19Fuar and array combinators
- 6:29Programs as index functions
- 8:17PartitionIndices index functions
- 12:11Permutation proof queries
- 13:38No duplicates with solver
- 17:39Prototype demo
- 19:07Q&A: Optimizations
- 20:14Q&A: Solver design
- 21:18Q&A: Unknown results
- 22:22Q&A: Remove variables
- 24:53Q&A: Future inference
related talks
19mAutomated Verification of Fundamental Algebraic Laws
20mA Mechanized Algebra of Verified Data Structures for Optimizing Sparse Tensor Programs
01h 01mFunction Composition in Programming Languages
18mA Verified Compiler for a Functional Tensor Language
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
32mDon’t Call Us, We’ll Call You
08mCompiling pattern matching to in-place modifications
15mCompilation of Sparse Array Programming Models