package coq-validsdp
ValidSDP
Install
Dune Dependency
Authors
Maintainers
Sources
validsdp-1.1.0.tar.gz
sha512=7ae0d6116dd81633fa5fcdbf3e28e8ba287229d6436350a2d0b13216191e9541e3c9312eb27c106c10f33df9cfcc67ccaf161f620e1a384efbfc98648b99fc7d
Description
ValidSDP is a library for the Coq formal proof assistant. It provides reflexive tactics to prove multivariate inequalities involving real-valued variables and rational constants, using SDP solvers as untrusted back-ends and verified checkers based on libValidSDP.
Once installed, you can import the following modules: From Coq Require Import Reals. From ValidSDP Require Import validsdp.
Tags
keyword:libValidSDP keyword:ValidSDP keyword:floating-point arithmetic keyword:Cholesky decomposition category:Miscellaneous/Coq Extensions logpath:ValidSDPPublished: 17 Sep 2025
Dependencies (12)
-
ocamlfind
build -
osdp
>= "1.1.1" -
coq-coqeal
>= "2.1" -
coq-mathcomp-multinomials
>= "2.0" -
coq-libvalidsdp
= version -
coq-mathcomp-reals-stdlib
>= "1.8.0" -
coq-mathcomp-field
>= "2.3" & < "2.5~" -
coq-interval
>= "4.0.0" & < "5~" -
coq-flocq
>= "3.3.0" - coq-bignums
-
coq
>= "9.0" & < "9.2~" - ocaml
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page