References

The following books: papers and blog posts serve as the basis for the algorithms used in the library:

  1. D. E. Knuth, The Art of Computer Programming, Volume 2: Seminumerical Algorithms, 3rd ed. Reading, MA, USA: Addison-Wesley, 1998.

  2. M. L. Scott and J. Aldrich, Programming Language Pragmatics, 5th ed. Burlington, MA, USA: Morgan Kaufmann, 2025.

  3. S. Klabnik, C. Nichols, and C. Krycho, The Rust Programming Language, ver. 1.90.0. San Francisco, CA, USA: No Starch Press, 2025.

  4. J.-M. Muller, N. Brisebarre, F. De Dinechin, C.-P. Jeannerod, V. Lefèvre, G. Melquiond, N. Revol, D. Stehlé, and S. Torres, Handbook of Floating-Point Arithmetic. Boston, MA, USA: Birkhäuser, 2000.

  5. B. C. Pierce, Types and Programming Languages. Cambridge, MA, USA: MIT Press, 2002.

  6. B. C. Pierce, Advanced Topics in Types and Programming Languages. Cambridge, MA, USA: MIT Press, 2005.

  7. S. Glesner, “Finite Integer Computations: An Algebraic Foundation for Their Correctness,” Formal Aspects of Computing, vol. 18, no. 2, pp. 244-262, 2006.

  8. R. Rieu-Helft, C. Marché, and G. Melquiond, “How to Get an Efficient yet Verified Arbitrary-Precision Integer Library,” in Verified Software. Theories, Tools, and Experiments (VSTTE 2017), A. Paskevich and T. Wies, Eds. Lecture Notes in Computer Science, vol. 10712. Cham, Switzerland: Springer, 2017, pp. 84-101.

  9. G. Melquiond and R. Rieu-Helft, "A Why3 framework for reflection proofs and its application to GMP’s algorithms," in Proc. 9th Int. Joint Conf. Automated Reasoning (IJCAR), Oxford, UK, Jul. 2018, vol. 10900, pp. 178–193.

  10. L. Valenty, "P2993 Constrained Numbers," https://wg21.link/p2993

Edit this Page