Questions tagged [floating-point]
Use this tag for floating point numbers as defined for use in a computer floating-point register. Do not use this tag for the mathematical concept of a floating point number.
3 questions
12
votes
3
answers
356
views
PDEs and proof assistants
I would like to know if there are any ongoing or completed projects in the area of the verification of the numerical methods for PDEs or the exposition of (any aspects of) the traditional PDE theory ...
20
votes
3
answers
546
views
How can I prove facts about floating point calculations?
In computing, there is a standard called IEEE 754. Unlike in mathematics, computers have to fit numbers into a finite amount of space; to do this, they use a format a bit like scientific notation, ...
12
votes
1
answer
88
views
Tools to check correctness of decimal floating point arithmetic
I have implemented (in TeX, but it doesn't matter for this question) a library of functions that evaluate basic arithmetic, as well as some transcendental functions such as cosine, on decimal floating ...