Skip to content
@validsdp

validsdp

Proving multivariate inequalities in Coq using SDP solvers and floating-point arithmetic

Popular repositories Loading

  1. validsdp validsdp Public

    A Coq tactic for proving multivariate inequalities using SDP solvers

    Rocq Prover 10 1

  2. coq-floats-jfla2021 coq-floats-jfla2021 Public

    Flottants primitifs en Coq / Démo (https://git.io/JYhpS)

    Coq 4

  3. unicoq unicoq Public

    Forked from unicoq/unicoq

    An enhanced unification algorithm for Coq

    OCaml 1

  4. Csdp Csdp Public

    Forked from coin-or/Csdp

    This is the working repository for the CSDP project. CSDP is a solver for semidefinite programming problems. It is a COIN-OR project.

    C 1

  5. coq coq Public

    Forked from rocq-prover/rocq

    Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive develo…

    OCaml

  6. bignums bignums Public

    Forked from rocq-community/bignums

    Coq library of arbitrary large numbers. Provides BigN, BigZ, BigQ that used to be part of Coq standard library

    Coq

Repositories

Showing 10 of 10 repositories

People

This organization has no public members. You must be a member to see who’s a part of this organization.

Top languages

Loading…

Most used topics

Loading…