coq-scev

Scalar evolution is an algebraic theory of recurrences. It has found use in modern compilers which use the theory to model loop variables. This is an implementation of the scalar evolution theory in Coq. In particular, it implements the definitions and simplification lemmas from the original "chains of recurrences" paper.

opam install coq-scev.1.0.1
homepage
https://github.com/bollu/SCEV-coq
license
MIT
bugs tracker
https://github.com/bollu/SCEV-coq/issues
dependencies
coq (>= 8.5 & < 8.6~)
source
https://github.com/bollu/SCEV-coq/releases/download/v1.1/coq-scev-v1.1.zip
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-scev/coq-scev.1.0.1