Marc Daumas, Laurence Rideau, Laurent Théry. A Generic Library for Floating-Point Numbers and Its Application to Exact Computing. In Richard J. Boulton, Paul B. Jackson, editors, Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Edinburgh, Scotland, UK, September 3-6, 2001, Proceedings. Volume 2152 of Lecture Notes in Computer Science, pages 169-184, Springer, 2001. [doi]