Skip to main content
SpringerLink
Log in

Strongly Typed Numerical Computations

  • Conference paper
  • First Online:
Formal Methods and Software Engineering (ICFEM 2018)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11232))

Included in the following conference series:

  • 1031 Accesses

Abstract

It is well-known that numerical computations may sometimes lead to wrong results because of roundoff errors. We propose an ML-like type system (strong, implicit, polymorphic) for numerical computations in finite precision, in which the type of an expression carries information on its accuracy. We use dependent types and a type inference which, from the user point of view, acts like ML type inference. Basically, our type system accepts expressions for which it may ensure a certain accuracy on the result of the evaluation and it rejects expressions for which a minimal accuracy on the result of the evaluation cannot be inferred. The soundness of the type system is ensured by a subject reduction theorem and we show that our type system is able to type implementations of usual simple numerical algorithms.

This work is supported by the Office for Naval Research Global under Grant NICOP N62909-18-1-2068 (Tycoon project). https://www.onr.navy.mil/en/Science-Technology/ONR-Global.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    https://gmplib.org/.

References

  1. ANSI/IEEE: IEEE Standard for Binary Floating-point Arithmetic (2008)

    Google Scholar 

  2. Atkinson, K.: An Introduction to Numerical Analysis, 2nd edn. Wiley, Hoboken (1989)

    MATH  Google Scholar 

  3. Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.: LUSTRE: a declarative language for programming synchronous systems. In: POPL, pp. 178–188. ACM Press (1987)

    Google Scholar 

  4. Damouche, N., Martel, M., Chapoutot, A.: Impact of accuracy optimization on the convergence of numerical iterative methods. In: Falaschi, M. (ed.) LOPSTR 2015. LNCS, vol. 9527, pp. 143–160. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-27436-2_9

    Chapter  MATH  Google Scholar 

  5. Damouche, N., Martel, M., Chapoutot, A.: Improving the numerical accuracy of programs by automatic transformation. STTT 19(4), 427–448 (2017)

    Article  Google Scholar 

  6. Darulova, E., Kuncak, V.: Sound compilation of reals. In: POPL 2014, pp. 235–248. ACM (2014)

    Google Scholar 

  7. Denis, C., de Oliveira Castro, P., Petit, E.: Verificarlo: checking floating point accuracy through Monte Carlo arithmetic. In: ARITH 2016, pp. 55–62. IEEE (2016)

    Google Scholar 

  8. Franco, A.D., Guo, H., Rubio-González, C.: A comprehensive study of real-world numerical bug characteristics. In: ASE, pp. 509–519. IEEE (2017)

    Google Scholar 

  9. Goubault, E.: Static analysis by abstract interpretation of numerical programs and systems, and FLUCTUAT. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 1–3. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38856-9_1

    Chapter  Google Scholar 

  10. Mentor Graphics Algorithmic C Datatypes, Software Version 2.6 edn. (2011). http://www.mentor.com/esl/catapult/algorithmic

  11. Lam, M.O., Hollingsworth, J.K., de Supinski, B.R., LeGendre, M.P.: Automatically adapting programs for mixed-precision floating-point computation. In: Supercomputing, ICS 2013, pp. 369–378. ACM (2013)

    Google Scholar 

  12. Martel, M.: Floating-point format inference in mixed-precision. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 230–246. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57288-8_16

    Chapter  Google Scholar 

  13. Milner, R., Harper, R., MacQueen, D., Tofte, M.: The Definition of Standard ML. MIT Press, Cambridge (1997)

    Google Scholar 

  14. Panchekha, P., Sanchez-Stern, A., Wilcox, J.R., Tatlock, Z.: Automatically improving accuracy for floating point expressions. In: PLDI, pp. 1–11. ACM (2015)

    Google Scholar 

  15. Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)

    MATH  Google Scholar 

  16. Pierce, B.C. (ed.): Advanced Topics in Types and Programming Languages. MIT Press, Cambridge (2004)

    MATH  Google Scholar 

  17. Rubio-Gonzalez, C., et al.: Precimonious: tuning assistant for floating-point precision. In: HPCNSA, pp. 27:1–27:12. ACM (2013)

    Google Scholar 

  18. Solovyev, A., Jacobsen, C., Rakamarić, Z., Gopalakrishnan, G.: Rigorous estimation of floating-point round-off errors with symbolic taylor expansions. In: Bjørner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 532–550. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-19249-9_33

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Laboratoire de Mathématiques et Physique (LAMPS), Université de Perpignan Via Domitia, Perpignan, France

    Matthieu Martel

Authors
  1. Matthieu Martel
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Matthieu Martel .

Editor information

Editors and Affiliations

  1. University of Auckland, Auckland, New Zealand

    Jing Sun

  2. Peking University, Beijing, China

    Meng Sun

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Martel, M. (2018). Strongly Typed Numerical Computations. In: Sun, J., Sun, M. (eds) Formal Methods and Software Engineering. ICFEM 2018. Lecture Notes in Computer Science(), vol 11232. Springer, Cham. https://doi.org/10.1007/978-3-030-02450-5_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-02450-5_12

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-02449-9

  • Online ISBN: 978-3-030-02450-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation