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.2.tar.gz
sha512=3366ceeed08bc3ac43cc825aa5e86bdb40a002645458abbd85f8bc0f0b5a7fec4cbb69e72f3122bd6e7d30a9052d3bb75532277459ee1921ccb60adc6da4afad

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: 13 Dec 2023

Dependencies (13)

  1. ocamlfind build
  2. osdp >= "1.0"
  3. coq-paramcoq >= "1.1.0"
  4. coq-coqeal >= "1.1.3"
  5. coq-mathcomp-multinomials >= "1.6"
  6. coq-libvalidsdp = version
  7. coq-mathcomp-analysis >= "0.3.5" & < "0.6.6~"
  8. coq-mathcomp-field >= "1.15" & < "1.19~"
  9. coq-interval >= "4.0.0" & < "5~"
  10. coq-flocq >= "3.3.0"
  11. coq-bignums
  12. coq >= "8.15" & < "8.19~"
  13. ocaml

Dev Dependencies (1)

  1. conf-autoconf build & dev

Used by

None

Conflicts

None