package coq-validsdp

  1. Overview
  2. No Docs
ValidSDP

Install

Dune Dependency

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

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.3.tar.gz
sha512=c24db26f6457e5e5e17f8a5674f1885488661e031ec27c167690344c00f23f5bd534081814f364911217998a3c3ded672f8b785665f4f82ff3d3b6daa84e3388

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

Published: 06 Jan 2025

Dependencies (13)

  1. ocamlfind build
  2. osdp >= "1.1.1"
  3. coq-paramcoq >= "1.1.0"
  4. coq-coqeal >= "2.0.2"
  5. coq-mathcomp-multinomials >= "2.0"
  6. coq-libvalidsdp = version
  7. coq-mathcomp-analysis >= "1.0.0" & < "1.7~"
  8. coq-mathcomp-field >= "2.1" & < "2.3~"
  9. coq-interval >= "4.0.0" & < "5~"
  10. coq-flocq >= "3.3.0"
  11. coq-bignums
  12. coq >= "8.18" & < "8.20~"
  13. ocaml

Dev Dependencies (1)

  1. conf-autoconf build & dev

Used by

None

Conflicts

None