Numerical Fuzz: A Type System for Rounding Error Analysis

on YouTube ↗21m

" summary

A new functional language Λnum offers a linear type system plus a novel graded monad to track local floating‑point rounding error and a sensitivity analysis to bound error amplification; the paper proves soundness relating denotational, ideal, and floating‑point semantics. A prototype type checker infers bounds that match worst‑case theoretical errors for Horner up to degree 100 (200 ops), scales to a 128×128 matrix multiply (~4 million ops) and often runs in milliseconds (example: 36 ms, largest benchmark ~18 minutes), outperforming prior tools.

AI-written summary · about

" chapters (12)

1. 0:00Introduction
2. 1:05Rounding error bounds in polynomial eval
3. 2:29Floating point semantics
4. 4:39Numerical Fuzz analysis
5. 6:04Graded monad for errors
6. 7:30Sensitivity analysis
7. 8:53Function composition errors
8. 9:57Prototype demo
9. 10:40Optimal error bounds
10. 11:44Performance and scalability
11. 12:49Summary and limitations
12. 13:37Q&A