Formalization of Double-Word Arithmetic, and Comments on “Tight and Rigorous Error Bounds for Basic Building Blocks of Double-Word Arithmetic” (Q5066604): Difference between revisions

Latest revision as of 11:47, 28 July 2024

scientific article; zbMATH DE number 7500134

Language	Label	Description	Also known as
English	Formalization of Double-Word Arithmetic, and Comments on “Tight and Rigorous Error Bounds for Basic Building Blocks of Double-Word Arithmetic”	scientific article; zbMATH DE number 7500134

Statements

instance of

scholarly article

0 references

title

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

0 references

0 references

0 references

ACM Transactions on Mathematical Software

0 references

publication date

29 March 2022

0 references

zbMATH Keywords

floating-point arithmetic

0 references

double-word arithmetic

0 references

double-double arithmetic

0 references

formalization

0 references

proof assistant

0 references

coq

0 references

MaRDI profile type

MaRDI publication profile

0 references

full work available at URL

https://doi.org/10.1145/3484514

0 references

cites work

Verified compilation of floating-point computations

0 references

Formalization of real analysis: a survey of proof assistants and libraries

0 references

Q5274886

0 references

Q4790659

0 references

A floating-point technique for extending the available precision

0 references

On relative errors of floating-point operations: Optimal bounds and applications

0 references

Tight and Rigorous Error Bounds for Basic Building Blocks of Double-Word Arithmetic

0 references

CAMPARY: Cuda Multiple Precision Arithmetic Library and Applications

0 references

Q4344097

0 references

Design, implementation and testing of extended and mixed precision BLAS

0 references

Quasi double-precision in floating point addition

0 references

A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program

0 references

Handbook of Floating-Point Arithmetic

0 references

Scalar fused multiply-add instructions produce floating-point matrix arithmetic provably accurate to the penultimate digit

0 references

Accurate Sum and Dot Product

0 references

Adaptive precision floating-point arithmetic and fast robust geometric predicates

0 references

Identifiers

DOI

10.1145/3484514

0 references

Mathematics Subject Classification ID

0 references

0 references

0 references

0 references

Sitelinks

Mathematics(1 entry)

mardi Publication:5066604

@@ Property / cites work @@
+Verified compilation of floating-point computations
+Normal rank
@@ Property / cites work @@
+Formalization of real analysis: a survey of proof assistants and libraries
+Normal rank
@@ Property / cites work @@
+Q5274886
@@ Property / cites work: Q5274886 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4790659
@@ Property / cites work: Q4790659 / rank @@
+Normal rank
@@ Property / cites work @@
+A floating-point technique for extending the available precision
+Normal rank
@@ Property / cites work @@
+On relative errors of floating-point operations: Optimal bounds and applications
+Normal rank
@@ Property / cites work @@
+Tight and Rigorous Error Bounds for Basic Building Blocks of Double-Word Arithmetic
+Normal rank
@@ Property / cites work @@
+CAMPARY: Cuda Multiple Precision Arithmetic Library and Applications
+Normal rank
@@ Property / cites work @@
+Q4344097
@@ Property / cites work: Q4344097 / rank @@
+Normal rank
@@ Property / cites work @@
+Design, implementation and testing of extended and mixed precision BLAS
+Normal rank
@@ Property / cites work @@
+Quasi double-precision in floating point addition
@@ Property / cites work: Quasi double-precision in floating point addition / rank @@
+Normal rank
@@ Property / cites work @@
+A mechanically checked proof of the AMD5/sub K/86/sup TM/ floating-point division program
+Normal rank
@@ Property / cites work @@
+Handbook of Floating-Point Arithmetic
@@ Property / cites work: Handbook of Floating-Point Arithmetic / rank @@
+Normal rank
@@ Property / cites work @@
+Scalar fused multiply-add instructions produce floating-point matrix arithmetic provably accurate to the penultimate digit
+Normal rank
@@ Property / cites work @@
+Accurate Sum and Dot Product
@@ Property / cites work: Accurate Sum and Dot Product / rank @@
+Normal rank
@@ Property / cites work @@
+Adaptive precision floating-point arithmetic and fast robust geometric predicates
+Normal rank