Bean: A Language for Backward Error Analysis
summary
Bean is a typed first-order language that encodes backward error via a graded coeffect system with strict linearity and a categorical semantics proving soundness. The implementation and prototype statically infer backward-error bounds for benchmarks (dot product, sum, matrix‑vector, polynomial evaluation, triangular solver), producing bounds that match worst-case theoretical bounds and running with quadratic scaling in floating‑point ops. It is the first static tool for backward error analysis.
AI-written summary · about
chapters (13)
- 0:00Bean introduction and goals
- 1:06Numerical results need trustworthy analysis
- 2:30Forward vs backward error analysis
- 3:55First static tool for backward errors
- 5:19Conceptual backward error analysis
- 7:05Dot product example and bounds
- 9:11Bean implementation and type inference
- 11:19All Bean programs guarantee backward errors
- 12:41Backward error lenses semantics
- 15:28Evaluation and benchmarks
- 17:10Summary of features
- 18:32Q&A
- 22:43Final Q&A on error models
related talks
19mSynthesizing Backward Error Bounds, Backward
29mTowards Exact Semantic Equivalence of Erlang BEAM Constructs: Lessons from Advanced(…)
19mPanel: Compilation Frameworks
28mBridging Syntax and Semantics of Lean Expressions in E-Graphs
19mA Dependently Typed Language with Dynamic Equality
20mBeePL: Correct-by-compilation kernel extensions
46mThe Calculated Typer (Functional Pearl)
36mBAML - A new programming language for building Agents