Accurate calculation of Euclidean norms using double-word arithmetic

DOI10.1145/3568672WikidataQ131113284 ScholiaQ131113284MaRDI QIDQ6599993FDOQ6599993

Authors: Vincent Lefèvre, Nicolas Louvet, Jean-Michel Muller, Joris Picot, Laurence Rideau

Publication date: 6 September 2024

Published in: ACM Transactions on Mathematical Software (Search for Journal in Brave)

zbMATH Keywords

proof assistant floating-point arithmetic formalization Euclidean norms overflow square-root underflow coq double-double arithmetic double-word arithmetic

Mathematics Subject Classification ID

Numerical analysis (65-XX)

Cites Work

Algorithm 978: Safe scaling in the level 1 BLAS
Remark on Algorithm 539
The mathematical-function computation handbook. Programming using the MathCW portable software library
Title not available (Why is that?)
Accuracy and Stability of Numerical Algorithms
Formalization of real analysis: a survey of proof assistants and libraries
Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
A floating-point technique for extending the available precision
Design, implementation and testing of extended and mixed precision BLAS
Faithfully rounded floating-point computations
Scalar fused multiply-add instructions produce floating-point matrix arithmetic provably accurate to the penultimate digit
A New Approach to Probabilistic Rounding Error Analysis
Arb: Efficient Arbitrary-Precision Midpoint-Radius Interval Arithmetic
On relative errors of floating-point operations: optimal bounds and applications
Quasi double-precision in floating point addition
Error estimates for the summation of real numbers with application to floating-point summation
Verified compilation of floating-point computations
Computer arithmetic and formal proofs. Verifying floating-point algorithms with the Coq system
Handbook of floating-point arithmetic
Efficient calculations of faithfully rounded \(l_2\)-norms of \(n\)-vectors
On Ziv's rounding test
Emulating Round-to-Nearest Ties-to-Zero “Augmented” Floating-Point Operations Using Round-to-Nearest Ties-to-Even Arithmetic
On the robustness of the 2Sum and Fast2Sum algorithms
Implementing complex elementary functions using exception handling
Tight and Rigorous Error Bounds for Basic Building Blocks of Double-Word Arithmetic
Formalization of Double-Word Arithmetic, and Comments on “Tight and Rigorous Error Bounds for Basic Building Blocks of Double-Word Arithmetic”
Midpoints and Exact Points of Some Algebraic Functions in Floating-Point Arithmetic
Algorithm 1014
Matrix Multiplication in Multiword Arithmetic: Error Analysis and Application to GPU Tensor Cores

Cited In (1)

Accurate complex Jacobi rotations

This page was built for publication: Accurate calculation of Euclidean norms using double-word arithmetic

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