Refined Remora: Constraining Array Shapes

on YouTube ↗21m

" summary

Extends Remora’s index language with refinement predicates and arithmetic so the type checker can express and verify shape arithmetic (plus, minus, multiply, divide), sequence operations and rank, then discharges those constraints to an SMT solver; claims decidable checking where possible, proves type soundness, and ships a Haskell implementation that typechecks real kernels including n‑dimensional convolution and a YOLO vision pipeline. Tradeoffs: richer predicates make some inferences undecidable and SMT nondeterminism can fail trivial cases, but the system successfully encodes and verifies many practical kernels.

AI-written summary · about

" chapters (19)

1. 0:00Refined Remora introduction
2. 0:42Remora and array types
3. 3:10Index polymorphism in Remora
4. 5:17Remora type system limits
5. 6:012D convolution problem
6. 8:31Refinement types intro
7. 9:53Refined kinds and pi types
8. 10:55Zero matrix type example
9. 11:37Type checker with SMT solver
10. 12:39Extended refined operations
11. 13:22Final convolution type
12. 13:42Future work
13. 14:26Q&A
14. 15:21Optimization signals
15. 16:23Dependent typing
16. 17:27Kernel integration
17. 19:55GPU programs with Remora
18. 20:15Q&A on memory access
19. 21:19Closing remarks