package rocq-laproof
LAProof: a library of formal proofs of accuracy and correctness for linear algebra programs
Install
Dune Dependency
Authors
Maintainers
Sources
v2.0.tar.gz
sha256=5acbe4498fc0fea7f4d0a687723c954dbd287eeec0430cbc7049eeb315d44a5c
Description
LAProof is a package of software and Rocq proofs that verify (1) C programs for linear algebra on dense and sparse matrices correctly implement the specified floating-point algorithms; and (2) those floating-point algorithms are accurate within stated concrete bounds.
Dependencies (14)
-
coq-libvalidsdp
>= "1.1.1" -
coq-vst-lib
>= "2.15.1~" -
coq-vst
>= "2.16~" - coq-mathcomp-finmap
- coq-mathcomp-reals-stdlib
- coq-mathcomp-algebra-tactics
- coq-mathcomp-analysis
- coq-mathcomp-algebra
-
coq-mathcomp-ssreflect
>= "2.4.0~" -
coq-vcfloat
>= "2.4.1~" - coq-interval
- coq-flocq
- rocq-stdlib
-
coq-core
>= "9.0"
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page