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

    Coq 9 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 coq/coq

    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 coq-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
  • validsdp Public

    A Coq tactic for proving multivariate inequalities using SDP solvers

    validsdp/validsdp’s past year of commit activity
    Coq 9 LGPL-2.1 1 1 0 Updated Dec 16, 2024
  • coq Public Forked from coq/coq

    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 development of machine-checked proofs.

    validsdp/coq’s past year of commit activity
    OCaml 0 LGPL-2.1 675 0 0 Updated Aug 22, 2024
  • bignums Public Forked from coq-community/bignums

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

    validsdp/bignums’s past year of commit activity
    Coq 0 LGPL-2.1 22 0 0 Updated Jun 20, 2024
  • platform Public Forked from coq/platform

    Multi platform setup for Coq, Coq libraries and tools

    validsdp/platform’s past year of commit activity
    Shell 0 CC0-1.0 52 0 0 Updated Apr 18, 2024
  • benchs-primitive-floats Public

    Benchmarks for https://github.com/validsdp/coq/tree/primitive-floats

    validsdp/benchs-primitive-floats’s past year of commit activity
    Coq 0 0 0 1 Updated Jul 28, 2023
  • 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.

    validsdp/Csdp’s past year of commit activity
    C 1 EPL-2.0 32 0 0 Updated Aug 12, 2022
  • coq-floats-jfla2021 Public

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

    validsdp/coq-floats-jfla2021’s past year of commit activity
    Coq 4 0 0 0 Updated Apr 9, 2021
  • flocq Public

    This is a working copy (non-official) of the Flocq repository. See https://gitlab.inria.fr/flocq/flocq

    validsdp/flocq’s past year of commit activity
    Coq 0 LGPL-3.0 0 0 0 Updated Dec 18, 2020
  • coq-interval Public

    Fork de coq-interval pour le stage de Benjamin

    validsdp/coq-interval’s past year of commit activity
    Coq 0 0 0 0 Updated Dec 15, 2020
  • unicoq Public Forked from unicoq/unicoq

    An enhanced unification algorithm for Coq

    validsdp/unicoq’s past year of commit activity
    OCaml 1 MIT 16 0 0 Updated Sep 11, 2019

Top languages

Loading…

Most used topics

Loading…