ARRAY 2025
as the organisers put it
Array-oriented programming unites two uncommon properties. As an abstraction, it directly mirrors high-level mathematical concepts commonly used in many fields from natural sciences over engineering to financial modeling. As a language feature, it exposes regular control flow, exhibits structured data dependencies, and lends itself to many types of program analysis. Furthermore, many modern computer architectures, particularly highly parallel architectures such as GPUs and FPGAs, are well-suited to efficiently execute array operations. The ARRAY series of workshops explores all aspects of ...
| title | author | length |
|---|---|---|
| Structuring Arrays with Algebraic Shapes | Jakub Bachurski, Alan Mycroft, Dominic Orchard | 31m |
A new array calculus called Star gives arrays structured shapes and indices as records and variants with structural subtyping, so indexing errors are prevented… | ||
| Kuiper: verified and efficient GPU programming | Guido Martínez, Jonáš Fiala, Abhinav Jangda, Angelica Aparecida Moreira, Nikhil Swamy, Tyler Sorensen | 30m |
Kuiper is a verified GPU language that uses dependent types and concurrent separation logic (built on F★/Pulse) to guarantee memory safety and race freedom for… | ||
| (De/Re)-Composition of Array Computations + An MDH-Based DSL for Array Computations | Ari Rasch, Richard Schulze | 55m |
MDH provides a formal high-level representation plus a low-level tiling/placement IR and a fully auto-tuned lowering pipeline that emits CUDA/OpenCL code; a… | ||
| Accelerating the Static Analysis of Neural Networks by Batch Representation of(…) | Guillaume Berthelot, Arnault Ioualalen, Matthieu Martel | 25m |
They convert affine forms into three tensors — one for centers, one for noise symbols and one for residuals — so linear, convolutional and many nonlinear… | ||
| Array Programming on GPUs: Challenges and Opportunities | Xinyi Li, Mark Baranowski, Harvey Dam, Ganesh Gopalakrishnan | 28m |
Binary instrumentation at the SASS/PEX level finds pervasive floating-point exceptions across 256 GPU ports and pinpoints kernels that produce NaNs or… | ||
| Gate Fusion Is Map Fusion | Martin Elsman, Troels Henriksen | 29m |
Claim: gate operations are exactly index-transformed maps on the global state vector, so map-map fusion implements gate fusion. Implementation: a Futhark… | ||
| Efficient array (and data) processing by leveraging structure | Amir Shaikhha | 56m |
Claims a compilation-based DSL called SDQL that represents relations, vectors and sparse tensors as semiring dictionaries, implements ~44 algebraic rewrite… | ||
| nothing matches | ||