TeIL: a type-safe imperative Tensor Intermediate Language
summary
Defines a small, imperative tensor IR with precise semantics and a mechanized Coq formalization that proves programs have no out‑of‑bounds tensor accesses (static memory safety) under its typing rules. Demonstrates a real bug class where wrong index/shape orderings produce segmentation faults and fixes it by restricting indexing and allowing controlled combinators instead of arbitrary index expressions. Implements a translator and a C code generator used in a CFD operator pipeline and limits transposes to adjacent‑dimension transposes for tractable proofs.
AI-written summary · about
chapters (8)
- 0:00Start
- 10:23Overview
- 12:55Type Safety
- 14:47Example with Matrix Multiplication
- 17:02Program Evaluation
- 18:12Rule for Valuated Statements
- 19:13Type Safety and Memory Safety
- 29:03Work in Progress
related talks
24mVerified Tensor-Program Optimization Via High-Level Scheduling Rewrites
18mA Verified Compiler for a Functional Tensor Language
04mInterview
16mThe Continuous Tensor Abstraction: Where Indices are Real
31mDependent tagless final
20mMimIR: An Extensible and Type-Safe Intermediate Representation for the DSL Age
18mGraph IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Af...
19mIll-Typed Programs Don't Evaluate