package coq-bertrand

  1. Overview
  2. No Docs
Correctness of Knuth's algorithm for prime numbers

Install

Dune Dependency

github.com Edit opam file Versions (8)

Authors

  1. L
    Laurent Théry

Maintainers

  1. P
    palmskog@gmail.com

Sources

v8.11.0.tar.gz
sha512=64ff110193197cba1a7858ae478c675727a4ff89ccccc1eeb70d857d8bcba1c0adc3786d73a9a605b1b92b9cd99a9fa8299548491307f23414d5700e65f84f4d

Description

A proof of correctness of the algorithm for computing prime numbers as described in "The Art of Computer Programming: Fundamental Algorithms" by Knuth, pp. 147-149, and an application using Bertrand's postulate.

Tags

category:Mathematics/Arithmetic and Number Theory/Number theory category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs based on external tools category:Miscellaneous/Extracted Programs/Arithmetic keyword:Knuth's algorithm keyword:prime numbers keyword:Bertrand's postulate logpath:Bertrand date:2020-08-21

Published: 21 Aug 2020

Dependencies (1)

  1. coq >= "8.8" & < "8.12~"

Dev Dependencies

None

Used by

None

Conflicts

None