A Tour of Formal Verification with Coq:Knuth's Algorithm for Prime Numbers

Laurent Théry (1)

1 LEMME - Software and mathematics

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 mechanized in the Coq proof system.

Mots clés: PRIME NUMBERS; BERTRAND'S POSTULATE; PROGRAM VERIFICATION; COQ

Domaines: Autre [cs.OH]

Laurent Théry. A Tour of Formal Verification with Coq:Knuth's Algorithm for Prime Numbers. RR-4600, INRIA. 2002. ⟨inria-00071985⟩