coq-libvalidsdp

LibValidSDP LibValidSDP is a library for the Coq formal proof assistant. It provides results mostly about rounding errors in the Cholesky decomposition algorithm used in the ValidSDP library which itself implements Coq tactics to prove multivariate inequalities using SDP solvers. Once installed, the following modules can be imported : From libValidSDP Require Import Rstruct.v misc.v real_matrix.v bounded.v float_spec.v fsum.v fcmsum.v binary64.v cholesky.v float_infnan_spec.v binary64_infnan.v cholesky_infnan.v flx64.v zulp.v coqinterval_infnan.v.

opam install coq-libvalidsdp.0.5
homepage
https://sourcesup.renater.fr/validsdp/
license
LGPL
bugs tracker
https://github.com/validsdp/validsdp/issues
dependencies
coq (>= 8.7 & < 8.9~) & coq-interval (>= 3 & < 4~) & coq-mathcomp-field (>= 1.7 & < 1.8~) & ocamlfind & camlp4 & coq-flocq (>= 3 & < 4~) & coq-bignums
source
https://github.com/validsdp/validsdp/releases/download/v0.5/libvalidsdp.0.5.tgz
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-libvalidsdp/coq-libvalidsdp.0.5