coq-streams

Specification of Eratosthene Sieve . Proof of Eratosthene Sieve formalised using streams encoded as greatest fixpoints. See paper: @InProceedings{LePa94, author = "F. Leclerc and C. Paulin-Mohring", title = "Programming with Streams in {Coq}. A case study : The Sieve of Eratosthenes", editor = "H. Barendregt and T. Nipkow", volume = 806, series = "LNCS", booktitle = "{Types for Proofs and Programs, Types' 93}", year = 1994, publisher = "Springer-Verlag" }

opam install coq-streams.8.5.0
homepage
https://github.com/coq-contribs/streams
license
LGPL 2
bugs tracker
https://github.com/coq-contribs/streams/issues
dependencies
coq (>= 8.5 & < 8.6~)
source
https://github.com/coq-contribs/streams/archive/v8.5.0.tar.gz
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-streams/coq-streams.8.5.0