Innocuous Double Rounding of Basic Arithmetic Operations

DOI10.6092/issn.1972-5787/4359zbMath1451.65061OpenAlexW2255550028MaRDI QIDQ5195257

Pierre Roux

Publication date: 18 September 2019

Full work available at URL: https://doaj.org/article/748fef18ca2444d08db615872c085d56

zbMATH Keywords

floating-point arithmeticCoqdouble rounding

Mathematics Subject Classification ID

Roundoff error (65G50) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

Floating-point arithmetic ⋮ Simulating Low Precision Floating-Point Arithmetic

Uses Software

• Coq
• Flocq

This page was built for publication: Innocuous Double Rounding of Basic Arithmetic Operations