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.1.tar.gz
sha512=7857ceb8e7e04c2771f4264f6612e63f753bfca92a13a38bb058e817fc3dec60a6357992a74318a5bf617231c30beec3f2ea15c45243bc0b8186ccca043f8f82

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: 20 Sep 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.1"
  7. coq-mathcomp-analysis >= "0.3.5" & < "0.5.4~"
  8. coq-mathcomp-field >= "1.13" & < "1.16~"
  9. coq-interval >= "4.0.0" & < "5~"
  10. coq-flocq >= "3.3.0"
  11. coq-bignums < "9~"
  12. coq >= "8.14" & < "8.17~"
  13. ocaml

Dev Dependencies (1)

  1. conf-autoconf build & dev

Used by

None

Conflicts

None