Title | ||
---|---|---|
Formal Correctness of Comparison Algorithms Between Binary64 and Decimal64 Floating-Point Numbers. |
Abstract | ||
---|---|---|
We present a full Coq formalisation of the correctness of some comparison algorithms between binary64 and decimal64 floating-point numbers, using computation intensive proofs and a continued fractions library built for this formalisation. |
Year | DOI | Venue |
---|---|---|
2017 | 10.1007/978-3-319-63501-9_3 | Lecture Notes in Computer Science |
Field | DocType | Volume |
Programming language,Floating point,Computer science,Correctness,Algorithm,Mathematical proof,Computation | Conference | 10381 |
ISSN | Citations | PageRank |
0302-9743 | 0 | 0.34 |
References | Authors | |
3 | 3 |
Name | Order | Citations | PageRank |
---|---|---|---|
Arthur Blot | 1 | 17 | 1.28 |
Jean-Michel Muller | 2 | 466 | 66.61 |
Laurent Théry | 3 | 456 | 41.21 |