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.1.tar.gz
sha256=b1eb1a91688bb316fe2be885c399b567263cb244acf165b5ee2ac055d3a37283
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 (13)
-
coq-vst-lib
>= "2.15.1~" -
coq-vst
>= "2.17" - coq-libvalidsdp
- coq-mathcomp-finmap
- rocq-mathcomp-zify
- rocq-mathcomp-reals-stdlib
- rocq-mathcomp-algebra
-
rocq-mathcomp-ssreflect
>= "2.6.0~" -
coq-vcfloat
>= "2.4.2~" - coq-interval
- coq-flocq
- rocq-stdlib
-
coq-core
>= "9.1~"
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page