PLDI 2025
Mon 16 - Fri 20 June 2025 Seoul, South Korea
Wed 18 Jun 2025 15:00 - 15:20 at Cosmos, Violet & Tulip - Numerics and Approximation Chair(s): Pavel Panchekha

\emph{Backward error analysis} offers a method for assessing the quality of numerical programs in the presence of floating-point rounding errors. However, techniques from the numerical analysis literature for quantifying backward error require substantial human effort, and there are currently no tools or automated methods for statically deriving sound backward error bounds. To address this gap, we propose Bean, a typed first-order programming language designed to express quantitative bounds on backward error. Bean’s type system combines a graded coeffect system with strict linearity to soundly track the flow of backward error through programs. We prove the soundness of our system using a novel categorical semantics, where every Bean program denotes a triple of related transformations that together satisfy a backward error guarantee.

To illustrate Bean's potential as a practical tool for automated backward error analysis, we implement a variety of standard algorithms from numerical linear algebra in Bean, establishing fine-grained backward error bounds via typing in a compositional style. We also develop a prototype implementation of Bean that infers backward error bounds automatically. Our evaluation shows that these inferred bounds match worst-case theoretical relative backward error bounds from the literature, underscoring Bean's utility in validating a key property of numerical programs: \emph{numerical stability}.

Wed 18 Jun

Displayed time zone: Seoul change

14:00 - 15:20
Numerics and ApproximationPLDI Research Papers at Cosmos, Violet & Tulip
Chair(s): Pavel Panchekha University of Utah
14:00
20m
Talk
Solving Floating-Point Constraints with Continuous Optimization
PLDI Research Papers
Qian Chen Nanjing University, Chenqi Cui Nanjing University, Fengjuan Gao Nanjing University of Science and Technology, Yu Wang Nanjing University, Ke Wang Visa Research, Linzhang Wang Nanjing University
DOI
14:20
20m
Talk
Support Triangle Machine
PLDI Research Papers
Jiaying Li R3 Lab, Chunxue Hao China CITIC Bank
DOI
14:40
20m
Talk
Correctly Rounded Math Libraries without Worrying about the Application’s Rounding Mode
PLDI Research Papers
Sehyeok Park Rutgers University, Justin Kim Rutgers University, Santosh Nagarakatte Rutgers University
DOI
15:00
20m
Talk
Bean: A Language for Backward Error Analysis
PLDI Research Papers
Ariel E. Kellison Cornell University, Laura Zielinski Cornell University, David Bindel Cornell University, Justin Hsu Cornell University
DOI