Skip to content

@validsdp validsdp

Change the repository type filter

All

    Repositories list

    10 repositories

    • validsdp

      Public
      A Coq tactic for proving multivariate inequalities using SDP solvers
      floating-pointsemidefinite-programmingcoq-librarycoq-tacticcholesky-decompositionmathcompcoq
      Coq
      •
      GNU Lesser General Public License v2.1
      •1•9•1•1•Updated Nov 8, 2024Nov 8, 2024

    • coq

      Public
      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.
      OCaml
      •
      GNU Lesser General Public License v2.1
      •658•0•0•0•Updated Aug 22, 2024Aug 22, 2024

    • bignums

      Public
      Coq library of arbitrary large numbers. Provides BigN, BigZ, BigQ that used to be part of Coq standard library
      Coq
      •
      GNU Lesser General Public License v2.1
      •22•0•0•0•Updated Jun 20, 2024Jun 20, 2024

    • platform

      Public
      Multi platform setup for Coq, Coq libraries and tools
      Shell
      •
      Creative Commons Zero v1.0 Universal
      •50•0•0•0•Updated Apr 18, 2024Apr 18, 2024

    • benchs-primitive-floats

      Public
      Benchmarks for https://github.com/validsdp/coq/tree/primitive-floats
      Coq
      •0•0•0•1•Updated Jul 28, 2023Jul 28, 2023

    • Csdp

      Public
      This is the working repository for the CSDP project. CSDP is a solver for semidefinite programming problems. It is a COIN-OR project.
      C
      •
      Eclipse Public License 2.0
      •31•1•0•0•Updated Aug 12, 2022Aug 12, 2022

    • coq-floats-jfla2021

      Public
      Flottants primitifs en Coq / Démo (https://git.io/JYhpS)
      coqfloating-point
      Coq
      •0•4•0•0•Updated Apr 9, 2021Apr 9, 2021

    • flocq

      Public
      This is a working copy (non-official) of the Flocq repository. See https://gitlab.inria.fr/flocq/flocq
      Coq
      •
      GNU Lesser General Public License v3.0
      •0•0•0•0•Updated Dec 18, 2020Dec 18, 2020

    • coq-interval

      Public
      Fork de coq-interval pour le stage de Benjamin
      Coq
      •
      Other
      •0•0•0•0•Updated Dec 15, 2020Dec 15, 2020

    • unicoq

      Public
      An enhanced unification algorithm for Coq
      OCaml
      •
      MIT License
      •16•1•0•0•Updated Sep 11, 2019Sep 11, 2019