[1] Sylvain Chevillard, Mioara Joldes, John Harrison, and Christoph Lauter. Efficient and accurate computation of upper bounds of approximation errors. Theoretical Computer Science, 412(16):1523--1543, April 2011. [ bib | DOI | http ]
Keywords: tools, approximation, formal proof, multiple precision
[2] Florent de Dinechin, Christoph Lauter, and Guillaume Melquiond. Certifying the floating-point implementation of an elementary function using Gappa. IEEE Transactions on Computers, 60(2):242--253, February 2011. [ bib | DOI | http | .pdf ]
Keywords: formal proofs
[3] S. Boldo and G. Melquiond. Flocq: A unified library for proving floating-point algorithms in Coq. In ARITH 20, page 243–252, 2011. [ bib | .pdf ]
Keywords: formal proof
[4] John Harrison. Formal verification of floating point trigonometric functions. In Formal Methods in Computer-Aided Design: Third International Conference FMCAD 2000, volume 1954 of Lecture Notes in Computer Science, pages 217--233. Springer-Verlag, 2000. [ bib ]
Keywords: formal proof, sin, cos
[5] John Harrison. Floating point verification in HOL light: The exponential function. In Algebraic Methodology and Software Technology, pages 246--260, 1997. [ bib | .html ]
Keywords: formal proof, exp
[6] Donald Knuth. The Art of Computer Programming, vol.2: Seminumerical Algorithms. Addison Wesley, 3rd edition, 1997. [ bib ]
Keywords: multiple precision, formal proof, division, textbook

This file was generated by bibtex2html 1.98.