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.12.0.tar.gz
sha512=5035f6424b94ae3dded0b7f7db7bd5cb419cdb0c5c07dd0a401d5f5a7ba991716a16757216f64b9f9f7fe16fec1a882b5f75b77266a69542c305cb03e351fdc1

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

Published: 11 Oct 2020

Dependencies (1)

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

Dev Dependencies

None

Used by

None

Conflicts

None