Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Bertrand's postulate

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Bertrand's postulate


chronological Thread 
  • From: Laurent Thery <Laurent.Thery AT sophia.inria.fr>
  • To: coq-club AT pauillac.inria.fr
  • Cc: Jean-Christophe.Filliatre AT lri.fr, Olivier.Desmettre AT inria.fr
  • Subject: [Coq-Club] Bertrand's postulate
  • Date: Tue, 05 Nov 2002 00:22:10 +0100
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Dear Coq Users,

A correctness proof of Knuth's algorithm for computing
the first prime numbers has just been completed in Coq.

The proof is based on a nice property of prime numbers 
called Bertrand's postulate that states that there is always
a prime number between n and 2n (n>2).

This proof is a nice example of the different kinds of verification
that are possible within Coq. 

More information on the proof is available at:

 ftp://ftp-sop.inria.fr/lemme/Laurent.Thery/Bertrand/index.html

Regards,

-- 
Laurent Thery     Phone (33) 4 92 38 78 16 e-mail 
Laurent.Thery AT inria.fr
Projet Lemme INRIA - Sophia Antipolis,
2004, route des Lucioles - B.P. 93 
06902 Sophia Antipolis Cedex France 

















Archive powered by MhonArc 2.6.16.

Top of Page