×
Muller, Jean-Michel; Rideau, Laurence

Formalization of double-word arithmetic, and comments on “Tight and rigorous error bounds for basic building blocks of double-word arithmetic”. (English) Zbl 07500134

ACM Trans. Math. Softw. 48, No. 1, Article No. 9, 24 p. (2022).

Cited in 2 Documents

MSC:

65-XX Numerical analysis

Keywords:

floating-point arithmetic; double-word arithmetic; double-double arithmetic; formalization; proof assistant; coq

Citations:

Zbl 1484.65103

Software:

Flocq; HOL Light; CAMPARY
Cite Review PDF
Full Text: DOI HAL

References:

[1] Boldo, Sylvie, Jourdan, Jacques-Henri, Leroy, Xavier, and Melquiond, Guillaume. 2015. Verified compilation of floating-point computations. Journal of Automated Reasoning54, 2 (2015), 135-163. DOI:doi:10.1007/s10817-014-9317-x · Zbl 1331.68047
[2] Boldo, Sylvie, Lelay, Catherine, and Melquiond, Guillaume. 2016. Formalization of real analysis: A survey of proof assistants and libraries. Mathematical Structures in Computer Science26, 7 (2016), 1196-1233. Retrieved from http://hal.inria.fr/hal-00806920. · Zbl 1364.68327
[3] Boldo, Sylvie and Melquiond, Guillaume. 2011. Flocq: A unified library for proving floating-point algorithms in Coq. In Proceedings of the 20th IEEE Symposium on Computer Arithmetic, 243-252. DOI:doi:10.1109/ARITH.2011.40
[4] Boldo, Sylvie and Melquiond, Guillaume. 2017. Computer Arithmetic and Formal Proofs. ISTE Press - Elsevier. · Zbl 1385.68001
[5] Coe, Tim and Tang, Ping Tak Peter. 1995. It takes six ones to reach a flaw. In Proceedings of the 12th IEEE Symposium on Computer Arithmetic, 140-146. DOI:doi:10.1109/ARITH.1995.465365
[6] Daumas, Marc, Rideau, Laurence, and Théry, Laurent. 2001. A generic library of floating-point numbers and its application to exact computing. In Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics, 169-184. · Zbl 1005.68544
[7] Dinechin, Florent de, Ershov, Alexey V., and Gast, Nicolas. 2005. Towards the Post-Ultimate libm. In Proceedings of the 17th IEEE Symposium on Computer Arithmetic, 288-295. DOI:doi:10.1109/ARITH.2005.46
[8] Dekker, Theodorus J.. 1971. A floating-point technique for extending the available precision. Numerische Mathematik18, 3 (1971), 224-242. · Zbl 0226.65034
[9] Harrison, John. 1997. Floating-Point Verification in HOL Light: The Exponential Function. Technical Report 428. University of Cambridge Computer Laboratory.
[10] Harrison, John. 1999. A machine-checked theory of floating point arithmetic. In Proceedings of the 12th International Conference in Theorem Proving in Higher Order Logics. Y. Bertot, G. Dowek, L. Théry, A. Hirschowitz, C. Paulin (Eds.), , Vol.1690. Springer-Verlag, Berlin, 113-130.
[11] Hida, Yozo, Li, Xiaoye S., and Bailey, David H.. 2001. Algorithms for quad-double precision floating-point arithmetic. In Proceedings of the 15th IEEE Symposium on Computer Arithmetic, 155-162. DOI:doi:10.1109/ARITH.2001.930115
[12] Hida, Yozo, Li, Xiaoye S., and Bailey, David H.. 2012. C++/Fortran-90 double-double and quad-double package. Retrieved March 2, 2017 from http://crd-legacy.lbl.gov/dhbailey/mpdist/.
[13] IEEE. 2019. IEEE standard for floating-point arithmetic. IEEE Std 754-2019 (Revision of IEEE 754-2008) (July2019), 1-84. Retrieved December 7, 2021 from doi:10.1109/IEEESTD.2019.8766229
[14] Isupov, Konstantin. 2020. Performance data of multiple-precision scalar and vector BLAS operations on CPU and GPU. Data in Brief30 (2020), 105506. DOI:doi:10.1016/j.dib.2020.105506
[15] Jeannerod, Claude-Pierre and Rump, Siegfried M.. 2018. On relative errors of floating-point operations: Optimal bounds and applications. Mathematics of Computation87, 310 (2018), 803-819. DOI:doi:10.1090/mcom/3234 · Zbl 1380.65082
[16] Joldeş, Mioara, Muller, Jean-Michel, and Popescu, Valentina. 2017. Tight and rigourous error bounds for basic building blocks of double-word arithmetic. ACM Transactions on Mathematical Software44, 2 (2017), 27 pages. DOI:doi:10.1145/3121432 · Zbl 1484.65103
[17] Joldeş, Mioara, Muller, Jean-Michel, Popescu, Valentina, and Tucker, Warwick. 2016. CAMPARY: Cuda multiple precision arithmetic library and applications. In Proceedings of the 5th International Congress on Mathematical Software.GM. Greuel, T. Koch, P. Paule, A. Sommese (Eds.), , Vol. 9725, 232-240. Retrieved from https://hal.archives-ouvertes.fr/hal-01312858. · Zbl 1435.65012
[18] Kahan, William M.. 1997. Lecture Notes on the Status of IEEE-754. (1997). Retrieved from http://www.cs.berkeley.edu/wkahan/ieee754status/IEEE754.PDF.
[19] Knuth, Donald E.. 1998. The Art of Computer Programming (3rd ed.). Vol. 2. Addison-Wesley, Reading, MA. · Zbl 0895.68054
[20] Li, Xiaoye S., Demmel, James, Bailey, David H., Henry, Greg, Hida, Yozo, Iskandar, Jimmy, Kahan, William, Kang, Suh Y., Kapur, Anil, Martin, Michael C., Thompson, Brandon J., Tung, Teresa, and Yoo, Daniel J.. 2002. Design, implementation and testing of extended and mixed precision BLAS. ACM Transactions on Mathematical Software28, 2 (2002), 152-205. · Zbl 1070.65523
[21] Li, Xiaoye S., Demmel, James, Bailey, David H., Henry, Greg, Hida, Yozo, Iskandar, Jimmy, Kahan, William, Kapur, Anil, Martin, Michael C., Tung, Teresa, and Yoo, Daniel J.. 2000. Design, Implementation and Testing of Extended and Mixed Precision BLAS. Technical Report 45991. Lawrence Berkeley National Laboratory. Retrieved from https://www.davidhbailey.com/dhbpapers/xblas-report.pdf. · Zbl 1070.65523
[22] Møller, Ole. 1965. Quasi double-precision in floating-point addition. BIT5, 1 (1965), 37-50. · Zbl 0131.15805
[23] Moore, J. Strother, Lynch, Tom, and Kaufmann, Matt. 1998. A mechanically checked proof of the correctness of the kernel of the AMD5K86 floating point division algorithm. IEEE Transactions on Computers47, 9 (Sept.1998), 913-926. · Zbl 1392.68051
[24] Muller, Jean-Michel, Brisebarre, Nicolas, Dinechin, Florent de, Jeannerod, Claude-Pierre, Lefèvre, Vincent, Melquiond, Guillaume, Revol, Nathalie, Stehlé, Damien, and Torres, Serge. 2010. Handbook of Floating-Point Arithmetic. Birkhäuser Boston. 572 pages. · Zbl 1197.65001
[25] Nievergelt, Yves. 2003. Scalar fused multiply-add instructions produce floating-point matrix arithmetic provably accurate to the penultimate digit. ACM Transactions on Mathematical Software29, 1 (2003), 27-48. · Zbl 1069.68505
[26] Ogita, Takeshi, Rump, Siegfried M., and Oishi, Shin’ichi. 2005. Accurate sum and dot product. SIAM Journal on Scientific Computing26, 6 (2005), 1955-1988. DOI:doi:10.1137/030601818 · Zbl 1084.65041
[27] Riedy, Jason and Demmel, James. 2018. Augmented arithmetic operations proposed for IEEE-754 2018. In Proceedings of the 25th IEEE Symposium on Computer Arithmetic, 45-52. DOI:doi:10.1109/ARITH.2018.8464813
[28] Shewchuk, Jonathan R.. 1997. Adaptive precision floating-point arithmetic and fast robust geometric predicates. Discrete Computational Geometry18, 3 (1997), 305-363. DOI:doi:10.1007/PL00009321 · Zbl 0892.68098
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.