ARRAY 2026
as the organisers put it
Array-oriented programming unites two properties that demand close synergy and interaction. As an abstraction, it directly reflects the high-level mathematical concepts that underlie fields ranging from the natural sciences and engineering to high-performance computing and financial modeling. As a language feature, it provides regular control flow, exposes structured data dependencies, supports view-based reshaping, manages sparsity, and–above all–lends itself naturally to a wide range of program analyses. The ARRAY workshop series examines all aspects of array programming, such as languag ...
who it's for
array language researchers, compiler engineers, gpu kernel developers, hpc application developers, programming language designers, formal verification engineers, data layout and performance engineers
topics
graded monoids for arrays; Lean 4 elaboration-time parsing; semantic equivalence checking for kernels; FX graph extraction pipelines; SMT-based shape and type checking; MLIR sparse coiteration vectorization; sparse tensor dialect lowering; linear-algebraic hypervisor execution; relational cell morphing verification; provenance-aware dimensional checking; declarative nested query language; tile and brick hierarchical layouts
| title | author | length |
|---|---|---|
| Graded Monoids for Dependently Typed Array Programming | Juuso Haavisto, Jeremy Gibbons | 21m |
Defines graded monoids as indexing algebras that let a single fold compute both values and index metadata, proven by a monoid-homomorphism that lifts to an… | ||
| Tensor Algebra Equivalence Checker | Jubi Taneja, Tom St. John, Natalie Serrino | 20m |
A semantic equivalence checker formally verifies whether an optimized PyTorch or Triton kernel computes the same function as its baseline for all inputs… | ||
| Refined Remora: Constraining Array Shapes | Vadym Matviichuk, Olin Shivers | 21m |
Extends Remora’s index language with refinement predicates and arithmetic so the type checker can express and verify shape arithmetic (plus, minus, multiply… | ||
| Welcoming Remarks | Ganesh Gopalakrishnan, Artjoms Šinkarovs | 04m |
Announces the 12th in the series, notes arrays regain urgency for sparsity and layout for GPU work, and explains the conference timing: a 20 vs 25 minute split… | ||
| Vectorizing Sparse Coiteration for Two-finger Loop Structure (Extended Abstract) | Kabilan Mahathevan, Kirshanthan Sundarararajah | 20m |
Proposes an MLIR optimization pass that turns compressed-hierarchy sparse co-iteration SCF loops into a dual-path execution: a predicated, vectorized fast lane… | ||
| Towards a Linear-Algebraic Hypervisor | Breandan Considine | 18m |
Describes a linear-algebraic hypervisor that compiles a tiny array language into a branch-free multilinear transition operator and executes thousands to… | ||
| Relational Cell Morphing: Automated Verification of Relational Properties of Array(…) | Weihao Qu, Marco Gaboardi, Hiroshi Unno, Eric Koskinen | 20m |
The system reduces relational verification of array programs to constrained Horn clause solving over scalars by tracking a few distinguished cells across two… | ||
| Semantics as a Tool of Thought: Provenance-Aware Dimensional Checking in a Reactive(…) | Christopher Buck | 05m |
A reactive array IR called Three-Graph Reactive Unit Array IR interns noun phrases to integer token IDs and stores them in three co‑indexed flat arrays —… | ||
| Rhyme: A Multi-Paradigm Declarative Query Language | Ran Guo, Tiark Rompf | 14m |
Rhyme is an implemented declarative language for nested data that expresses aggregations, group-bys, joins and tensor ops in a single JSON-like syntax and… | ||
| Tiles, Bricks, and Layouts: How Aggregate Data Abstractions Aid in Optimizing Data(…) | Mary Hall | 01h 05m |
BrickLib packs work and data into 8x8x8 bricks stored contiguously to avoid local packing and reduce off-node reorganization, driving stencil runs close to… | ||
| Leveraging AI Ecosystem for Portable and Sustainable GPU Kernels in HPC | Yanbo Zhao, Zhaonan Meng, Sai Krishna Teja Varma Manthena, Xu Liu, Ajay Panyala, Jiajia Li | 25m |
A compilation framework converts Triton kernels into standalone shared objects with C APIs, removing Python/PyTorch dependencies and loading PTX/cubin/fatbin… | ||
| The Shape of Things to Come | Jared Roesch | 01h 00m |
A Python/C++/Rust DSL (cuTile) plus an MLIR-based array ISA (TileIR) targets portable, tile-level CUDA kernels that shift memory movement and tiling into the… | ||
| nothing matches | ||