| Web Site | https://manu.sridharan.net |
| https://twitter.com/rakingleaves | |
| GitHub | https://github.com/msridhar |
| https://www.linkedin.com/in/manusridharan |
A new piece of research as part of my group's safe and formally verified numerics project that I am really excited about -- The FLoPS framework, which formalizes the upcoming P3109 standard in Lean. Great work by my PhD students: Tung-Che Chang and Sehyeok Park and collaborator Jay Lim from University of California, Riverside.
The upcoming IEEE-P3109 standard for low-precision floating-point arithmetic can become the foundation of future machine learning hardware and software. Unlike the fixed types of IEEE-754, P3109 introduces a parametric framework defined by bitwidth, precision, signedness, and domain. This flexibility results in a vast combinatorial space of formats -- some with as little as one bit of precision -- alongside novel features such as stochastic rounding and saturation arithmetic.
We have formalized the P3109 standard and discovered new interesting properties of foundational algorithms such as Fast2Sum, Sternbenz, and a floating-point splitting ExtractScalar in the context of P3109.
During this process, we discovered some errors in the draft standard and reported it to the working group (I am member of the P3109 working group). They have been fixed.
See the Github repo of our mechanized proofs in Lean: https://github.com/rutgers-apl/flops
See our technical report:
https://arxiv.org/pdf/2602.15965
On a side note, I was convincingly persuaded to explore Lean by Ilya Sergey when I visited NUS in August 2024. Thanks Ilya for making a compelling case for using Lean while Umang Mathur and Abhik Roychoudhury made the visit possible.
Choreographies are coordination plans for concurrent and distributed systems, which define the roles of the involved participants and how they are supposed to work together. In the paradigm of choreographic programming (CP), choreographies are programs that can be compiled to executable implementations. CP originated primarily in the context of process calculi, with preliminary work done to establish its foundations and experiment with implementations. Recently, several proposals have shown that one can adapt CP to work in synergy with mainstream programming paradigms, such as object-orien ...
👋 Hi everyone, I’m enabling GitHub Sponsors for Metro
If Metro has improved your developer experience or saved your team's build times, I’d appreciate the support!
Full pitch and ROI napkin math here: https://www.zacsweers.dev/sponsoring-metro/
Metro is the proudest work of my career. Ever since starting it on vacation in November 2024, building it has been an incredible journey and the community reception has been nothing short of wonderful. It sits at the intersection of several fields I've come to specialize in, ranging from metaprogramming
Speaking truth to power in both senses of the word.
Highly recommended:
An interview with Nvidia's senior VP of hardware engineering, Andrew Bell, on continuing to provide Shield Android TV software updates a decade after its launch (Ryan Whitwam/Ars Technica)
https://arstechnica.com/gadgets/2026/01/inside-nvidias-10-year-effort-to-make-the-shield-tv-the-most-updated-android-device-ever/
http://www.techmeme.com/260131/p16#a260131p16
Adrian Sampson
Santosh Nagarakatte
Andrew K. Hirsch
Zac Sweers
Craig Hockenberry
Techmeme
Shriram Krishnamurthi
Jonathan Aldrich