Skip to main content
SpringerLink
Log in

Proving Pearl: Knuth’s Algorithm for Prime Numbers

  • Conference paper
Theorem Proving in Higher Order Logics (TPHOLs 2003)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2758))

Included in the following conference series:

Abstract

In his book “The Art of Computer Programming”, Donald Knuth gives an algorithm to compute the first n prime numbers. Surprisingly, proving the correctness of this simple algorithm from basic principles is far from being obvious and requires a wide range of verification techniques. In this paper, we explain how the verification has been mechanised in the Coq proof system.

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 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Agrawal, M., Kayal, N., Saxena, N.: PRIMES is in P. Preprint (2002), Available at http://www.cse.iit.ac.in/primality.pdf

  2. Aigner, M., Ziegler, G.M.: Proofs from THE BOOK. Springer, Heidelberg (1998)

    MATH  Google Scholar 

  3. Almeida, J.C., Théry, L.: Correctness of the RSA algorithm. Coq contribution (1999), Available at http://coq.inria.fr/contribs/summary.html

  4. Bertot, Y., Magaud, N., Zimmermann, P.: A GMP program computing square roots and its proof within Coq. Journal of Automated Reasoning 29(3-4) (2002)

    Google Scholar 

  5. Caprotti, O., Oostdijk, M.: Formal and Efficient Primality Proofs by Use of Computer Algebra Oracles. Journal of Symbolic Computation 32(1), 55–70 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  6. Erdös, P.: Beweis eines Satzes von Tschebyschef. Acta Scientifica Mathematica 5, 194–198 (1932)

    MATH  Google Scholar 

  7. Filliâtre, J.-C.: Proof of Imperative Programs in Type Theory. In: Altenkirch, T., Naraschewski, W., Reus, B. (eds.) TYPES 1998. LNCS, vol. 1657, p. 78. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  8. Harrison, J.: Floating Point Verification in HOL. In: Schubert, E.T., Alves-Foss, J., Windley, P. (eds.) HUG 1995. LNCS, vol. 971, pp. 186–199. Springer, Heidelberg (1995)

    Google Scholar 

  9. Harrison, J., Théry, L.: A Skeptic’s Approach to Combining HOL and Maple. Journal of Automated Reasoning 21(3), 279–294 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  10. Hoare, C.A.R.: An Axiomatic Basis for Computer Programming. Communication of the ACM 12(10), 576–580, 583 (1969)

    Article  MATH  Google Scholar 

  11. Hurd, J.: Formal Verification of Probabilistic Algorithms. Phd Thesis, University of Cambridge (2002)

    Google Scholar 

  12. Knuth, D.E.: The Art of Computer Programming: Fundamental Algorithms, pp. 147–149. Addison-Wesley, Reading (1997)

    MATH  Google Scholar 

  13. PCoq. A Graphical User-interface to Coq, Available at http://www-sop.inria.fr/lemme/pcoq/

  14. Quaife, A.: Automated development of fundamental mathematical theories. Automated reasoning series, vol. 2. Kluwer, Dordrecht (1992)

    MATH  Google Scholar 

  15. Slinko, A.: Number Theory. Tutorial 5: Bertrand’s Postulate, Available at http://matholymp.com/tutorials/bertrand.pdf

  16. Théry, L.: A Tour of Formal Verification with Coq: Knuth’s Algorithm for Prime Numbers. Research Report 4600, INRIA (2002)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA, 2004 route des Lucioles, 06902, Sophia Antipolis, France

    Laurent Théry

Authors
  1. Laurent Théry
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Information Security Group, Dep. of Computer Science, ETH Zurich, Switzerland

    David Basin

  2. Computer Science Dept., Saarland University, 66123, Saarbrücken, Germany

    Burkhart Wolff

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Théry, L. (2003). Proving Pearl: Knuth’s Algorithm for Prime Numbers. In: Basin, D., Wolff, B. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2003. Lecture Notes in Computer Science, vol 2758. Springer, Berlin, Heidelberg. https://doi.org/10.1007/10930755_20

Download citation

  • DOI: https://doi.org/10.1007/10930755_20

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-40664-8

  • Online ISBN: 978-3-540-45130-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation