coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Bertrand's postulate, Laurent Thery
Archive powered by MhonArc 2.6.16.