Repository navigation

SCEV-coq

Public

About

LLVM's loop analysis theory (Scalar Evolution) formalized in Coq

10 stars

0 watching

Report repository

Name		Name	Last commit message	Last commit date
coq		coq
reading		reading
.depend		.depend
.gitignore		.gitignore
Make		Make
Makefile		Makefile
README.md		README.md
_CoqProject		_CoqProject
configure.sh		configure.sh
coq-scev.opam		coq-scev.opam
opam		opam

Repository files navigation

SCEV-coq

This is an implementation of the scalar evolution theory in Coq. In particular, it implements the math behind the "chains of recurrences" paper.

Core types

Changelog

v1.0 first release

References

About

LLVM's loop analysis theory (Scalar Evolution) formalized in Coq

10 stars

0 watching

Report repository

Releases

Packages

Contributors

Languages