package coq-validsdp

  1. Overview
  2. No Docs
ValidSDP

Install

Dune Dependency

sourcesup.renater.fr Edit opam file Versions (5)

Authors

  1. Ã
    Érik Martin-Dorel <erik.martin-dorel@irit.fr>
  2. P
    Pierre Roux <pierre.roux@onera.fr>

Maintainers

  1. Ã
    Érik Martin-Dorel <erik.martin-dorel@irit.fr>
  2. P
    Pierre Roux <pierre.roux@onera.fr>

Sources

validsdp-1.0.0.tar.gz
sha512=94d872eb3ef308cc7c344f3c39e60d5bc265b05bc6c50b2399475e1ac4e105b330b1d63cf4193a04388b7a173f142e246bb6b6c46092fe9c221ed85b1d6b7c3f

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:ValidSDP

Published: 25 Jan 2022

Dependencies (13)

  1. ocamlfind build
  2. osdp >= "1.0"
  3. coq-paramcoq >= "1.1.0"
  4. coq-coqeal >= "1.1.0"
  5. coq-mathcomp-multinomials >= "1.2"
  6. coq-libvalidsdp = "1.0.0"
  7. coq-mathcomp-analysis >= "0.3.4" & < "0.4~"
  8. coq-mathcomp-field >= "1.12" & < "1.15~"
  9. coq-interval >= "4.0.0" & < "5~"
  10. coq-flocq >= "3.3.0"
  11. coq-bignums < "9~"
  12. coq >= "8.12" & < "8.16~"
  13. ocaml

Dev Dependencies (1)

  1. conf-autoconf build & dev

Used by

None

Conflicts

None