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-0.6.0.tar.gz
sha256=ba7de610de209cce431bc93ff599ac21eb14d649a815ec9cfae27e064d0ea3bf

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: 24 Nov 2019

Dependencies (12)

  1. ocamlfind build
  2. osdp >= "1.0"
  3. coq-paramcoq >= "1.1.0"
  4. coq-coqeal >= "1.0.0"
  5. coq-mathcomp-multinomials >= "1.2"
  6. coq-libvalidsdp = "0.6.0"
  7. coq-mathcomp-field >= "1.8" & < "1.10~"
  8. coq-interval >= "3.4.0" & < "4~"
  9. coq-flocq >= "3.1.0"
  10. coq-bignums
  11. coq >= "8.7" & < "8.11~"
  12. ocaml

Dev Dependencies (1)

  1. conf-autoconf build & dev

Used by

None

Conflicts

None