validsdp

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

Pinned Repositories

benchs-primitive-floats
Benchmarks for https://github.com/validsdp/coq/tree/primitive-floats
Language:Coq0 3 00
bignums
Coq library of arbitrary large numbers. Provides BigN, BigZ, BigQ that used to be part of Coq standard library
Language:Coq0 3 00
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.
Language:OCaml0 3 00
coq-floats-jfla2021
Flottants primitifs en Coq / Démo (https://git.io/JYhpS)
Language:Coq4 3 00
coq-interval
Fork de coq-interval pour le stage de Benjamin
Language:Coq0 4 00
Csdp
This is the working repository for the CSDP project. CSDP is a solver for semidefinite programming problems. It is a COIN-OR project.
Language:C10
flocq
This is a working copy (non-official) of the Flocq repository. See https://gitlab.inria.fr/flocq/flocq
Language:Coq0 3 00
platform
Multi platform setup for Coq, Coq libraries and tools
Language:Shell00
unicoq
An enhanced unification algorithm for Coq
Language:OCaml1 2 00
validsdp
A Coq tactic for proving multivariate inequalities using SDP solvers
Language:Coq9 4 61

validsdp/validsdp
A Coq tactic for proving multivariate inequalities using SDP solvers
Language:Coq9 4 61
validsdp/coq-floats-jfla2021
Flottants primitifs en Coq / Démo (https://git.io/JYhpS)
Language:Coq4 3 00
validsdp/Csdp
This is the working repository for the CSDP project. CSDP is a solver for semidefinite programming problems. It is a COIN-OR project.
Language:C10
validsdp/unicoq
An enhanced unification algorithm for Coq
Language:OCaml1 2 00
validsdp/benchs-primitive-floats
Benchmarks for https://github.com/validsdp/coq/tree/primitive-floats
Language:Coq0 3 00
validsdp/bignums
Coq library of arbitrary large numbers. Provides BigN, BigZ, BigQ that used to be part of Coq standard library
Language:Coq0 3 00
validsdp/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.
Language:OCaml0 3 00
validsdp/coq-interval
Fork de coq-interval pour le stage de Benjamin
Language:Coq0 4 00
validsdp/flocq
This is a working copy (non-official) of the Flocq repository. See https://gitlab.inria.fr/flocq/flocq
Language:Coq0 3 00
validsdp/platform
Multi platform setup for Coq, Coq libraries and tools
Language:Shell00