Formalization of Double-Word Arithmetic, and Comments on “Tight and Rigorous Error Bounds for Basic Building Blocks of Double-Word Arithmetic”
From MaRDI portal
Publication:5066604
DOI10.1145/3484514OpenAlexW4213324292WikidataQ113309853 ScholiaQ113309853MaRDI QIDQ5066604
Jean-Michel Muller, Laurence Rideau
Publication date: 29 March 2022
Published in: ACM Transactions on Mathematical Software (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/3484514
floating-point arithmeticproof assistantformalizationcoqdouble-double arithmeticdouble-word arithmetic
Related Items (1)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Adaptive precision floating-point arithmetic and fast robust geometric predicates
- Verified compilation of floating-point computations
- A floating-point technique for extending the available precision
- CAMPARY: Cuda Multiple Precision Arithmetic Library and Applications
- Formalization of real analysis: a survey of proof assistants and libraries
- Handbook of Floating-Point Arithmetic
- A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program
- Tight and Rigorous Error Bounds for Basic Building Blocks of Double-Word Arithmetic
- On relative errors of floating-point operations: Optimal bounds and applications
- Quasi double-precision in floating point addition
- Scalar fused multiply-add instructions produce floating-point matrix arithmetic provably accurate to the penultimate digit
- Design, implementation and testing of extended and mixed precision BLAS
- Accurate Sum and Dot Product
This page was built for publication: Formalization of Double-Word Arithmetic, and Comments on “Tight and Rigorous Error Bounds for Basic Building Blocks of Double-Word Arithmetic”