Verified tensor-program optimization via high-level scheduling rewrites
<jats:p>We present a lightweight Coq framework for optimizing tensor kernels written in a pure, functional array language. Optimizations rely on user scheduling using series of verified, semantics-preserving rewrites. Unusually for compilation targeting imperative code with arrays and nested l...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Association for Computing Machinery (ACM),
2022-07-19T13:14:37Z.
|
| Subjects: | |
| Online Access: | Get fulltext |