Formalization of Double-Word Arithmetic, and Comments on “Tight and Rigorous Error Bounds for Basic Building Blocks of Double-Word Arithmetic”

DOI10.1145/3484514MaRDI QIDQ5066604zbMATH OpenOpenAlexWikidataFDO

Authors 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

zbMATH Keywords

proof assistantfloating-point arithmeticformalizationcoqdouble-double arithmeticdouble-word arithmetic

Mathematics Subject Classification ID

Numerical analysis (65-XX)

Cites work

• scientific article; zbMATH DE number 1033192 (Why is no real title available?)
• scientific article; zbMATH DE number 1863384 (Why is no real title available?)
• A floating-point technique for extending the available precision
• A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program
• Accurate Sum and Dot Product
• Adaptive precision floating-point arithmetic and fast robust geometric predicates
• CAMPARY: CUDA multiple precision arithmetic library and applications
• Computer arithmetic and formal proofs. Verifying floating-point algorithms with the Coq system
• Design, implementation and testing of extended and mixed precision BLAS
• Formalization of real analysis: a survey of proof assistants and libraries
• Handbook of Floating-Point 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
• Tight and Rigorous Error Bounds for Basic Building Blocks of Double-Word Arithmetic
• Verified compilation of floating-point computations

Cited in

(3)

• Floating-point arithmetic
• Accurate calculation of Euclidean norms using double-word arithmetic
• Tight and Rigorous Error Bounds for Basic Building Blocks of Double-Word Arithmetic

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”

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5066604)