The Wayback Machine - https://web.archive.org/web/20240314142156/https://github.com/validsdp/
Skip to content
@validsdp

validsdp

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

Popular repositories

  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. 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

  5. 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

  6. benchs-primitive-floats benchs-primitive-floats Public

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

    Coq

Repositories

Showing 8 of 8 repositories

Top languages

Loading…

Most used topics

Loading…