Formal Verification of Floating Point Trigonometric Functions

1. D. Bailey, P. Borwein, and S. Plouffe. On the rapid computation of various polylogarithmic constants. Mathematics of Computation, 66:903–913, 1997.

   Article  MATH  MathSciNet  Google Scholar 

2. A. Baker. A Consise Introduction to the Theory of Numbers. Cambridge University Press, 1985.

   Google Scholar 

3. G. Cousineau and M. Mauny. The Functional Approach to Programming. Cam-bridge University Press, 1998.

   Google Scholar 

4. T. J. Dekker. A floating-point technique for extending the available precision. Numerical Mathematics, 18:224–242, 1971.

   Article  MATH  MathSciNet  Google Scholar 

5. M. J. C. Gordon, R. Milner, and C. P. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979.

   Google Scholar 

6. R. L. Graham, D. E. Knuth, and O. Patashnik. Concrete Mathematics: A Foun-dation for Computer Science. Addison-Wesley, 2nd edition, 1994.

   Google Scholar 

7. J. Harrison. HOL Light: A tutorial introduction. In M. Srivas and A. Camilleri, editors, Proceedings of the First International Conference on Formal Methods in Computer-Aided Design (FMCAD’96), volume 1166 of Lecture Notes in mputerScience, pages 265–269. Springer-Verlag, 1996.

   Google Scholar 

8. J. Harrison. Verifying the accuracy of polynomial approximations in HOL. In E. L. Gunter and A. Felty, editors, Theorem Proving in Higher Order Logics: 10th International Conference, TPHOLs’97, volume 1275 of Lecture Notes in Computer Science, pages 137–152, Murray Hill, NJ, 1997. Springer-Verlag.

   Google Scholar 

9. J. Harrison. Theorem Proving with the Real Numbers. Springer-Verlag, 1998. Revised version of author’s PhD thesis.

   Google Scholar 

10. J. Harrison. A machine-checked theory of floating point arithmetic. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Théry, editors, Theorem Proving in Higher Order Logics: 12th International Conference, TPHOLs’99, volume 1690 of Lecture Notes in Computer Science, pages 113–130, Nice, France, 1999. Springer-Verlag.

    Google Scholar 

11. J. Harrison, T. Kubaska, S. Story, and P. Tang. The computation of transcendental functions on the IA-64 architecture. Intel Technology Journal, 1999-2Q4:1–7, 1999. This paper is available on the Web as http://developer.intel.com/technology/itj/q41999/articles/art_5.htm

    Google Scholar 

12. O. Møller. Quasi double-precision in floating-point addition. BIT, 5:37–50, 1965.

    Article  MATH  Google Scholar 

13. M. E. Remes. Sur le calcul effectif des polynomes d'approximation de Tchebichef. Comptes Rendus Hebdomadaires des Séances de l'Académie des Sciences, 199:337–340, 1934.

    MATH  Google Scholar 

14. P. H. Sterbenz. Floating-Point Computation. Prentice-Hall, 1974.

    Google Scholar 

15. S. Story and P. T. P. Tang. New algorithms for improved transcendental functions on IA-64. In I. Koren and P. Kornerup, editors, Proceedings, 14th IEEE symposium on on computer arithmetic, pages 4–11, Adelaide, Australia, 1999. IEEE Computer Society.

    Google Scholar 

16. P. T. P. Tang. Table-lookup algorithms for elementary functions and their error analysis. In Proceedings of the 10th Symposium on Computer Arithemtic, pages 232–236, 1991.

    Google Scholar 

17. P. Weis and X. Leroy. Le langage Caml. InterEditions, 1993. See also the CAML Web page: http://pauillac.inria.fr/caml/

Download references