Compiler representations & iteration models
Etch: Indexed Streams
A Lean 4 compiler and formalization of indexed streams — an operational intermediate representation for the fused execution of contraction programs across sparse tensor and relational algebra.
The problem
Sparse tensor algebra and relational algebra share the same underlying pattern — fused iteration over contractions — but are usually compiled by separate, informally specified systems.
The idea
Capture that shared pattern as *indexed streams*, a small operational IR with a formal semantics, so a single verified compiler can fuse and execute both tensor and relational contractions.
How it fits the group's work
Indexed streams give the group a formal account of the iteration model that underlies sparse compilation. By formalizing it in Lean 4 and showing it spans both tensor and relational algebra, Etch strengthens the claim that a single compiler abstraction can serve computations that are usually treated as unrelated.