-
ONERA
- Toulouse
-
coq-nix-toolbox Public
Forked from coq-community/coq-nix-toolboxNix helper scripts to automate local builds and CI [maintainers=@CohenCyril,@Zimmi48]
Nix MIT License UpdatedDec 4, 2024 -
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…
-
nixpkgs Public
Forked from NixOS/nixpkgsNix Packages collection & NixOS
Nix MIT License UpdatedDec 4, 2024 -
coq-lsp Public
Forked from ejgallego/coq-lspVisual Studio Code Extension and Language Server Protocol for Coq
OCaml GNU Lesser General Public License v2.1 UpdatedDec 4, 2024 -
coq-elpi Public
Forked from LPCIC/coq-elpiCoq plugin embedding elpi
OCaml GNU Lesser General Public License v2.1 UpdatedDec 4, 2024 -
coq-tools Public
Forked from JasonGross/coq-toolsSome scripts to help construct small reproducing examples of bugs, implement [Proof using], etc.
Python MIT License UpdatedDec 3, 2024 -
metacoq Public
Forked from MetaCoq/metacoqMetaprogramming in Coq
Coq MIT License UpdatedDec 3, 2024 -
analysis Public
Forked from math-comp/analysisMathematical Components compliant Analysis Library
Coq Other UpdatedDec 3, 2024 -
Coq-Equations Public
Forked from mattam82/Coq-EquationsA function definition package for Coq
Coq GNU Lesser General Public License v2.1 UpdatedDec 2, 2024 -
coqutil Public
Forked from mit-plv/coqutilCoq library for tactics, basic definitions, sets, maps
Coq MIT License UpdatedDec 2, 2024 -
fiat-crypto Public
Forked from mit-plv/fiat-cryptoCryptographic Primitive Code Generation by Fiat
Coq Other UpdatedNov 28, 2024 -
opam-coq-archive Public
Forked from coq/opamArchive for all Coq related OPAM packages organized in various repositories
OCaml GNU Lesser General Public License v2.1 UpdatedNov 12, 2024 -
hierarchy-builder Public
Forked from math-comp/hierarchy-builderHigh level commands to declare a hierarchy based on packed classes
Prolog MIT License UpdatedNov 12, 2024 -
-
odd-order Public
Forked from math-comp/odd-orderThe formal proof of the Odd Order Theorem
Coq UpdatedOct 30, 2024 -
QuickChick Public
Forked from QuickChick/QuickChickRandomized Property-Based Testing Plugin for Coq
Coq Other UpdatedOct 28, 2024 -
coq-serapi Public
Forked from rocq-archive/coq-serapiCoq Protocol Playground with Se(xp)rialization of Internal Structures.
OCaml Other UpdatedOct 16, 2024 -
coq-json Public
Forked from liyishuai/coq-jsonJSON in Coq
Coq BSD 3-Clause "New" or "Revised" License UpdatedOct 14, 2024 -
kami Public
Forked from mit-plv/kamiA Platform for High-Level Parametric Hardware Specification and its Modular Verification
Coq MIT License UpdatedSep 23, 2024 -
coq-performance-tests Public
Forked from coq-community/coq-performance-testsA library of Coq source files testing for performance regressions on Coq [maintainer=@JasonGross]
Coq MIT License UpdatedSep 21, 2024 -
rewriter Public
Forked from mit-plv/rewriterReflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting
Coq Other UpdatedSep 20, 2024 -
VST Public
Forked from PrincetonUniversity/VSTVerified Software Toolchain
Coq Other UpdatedSep 19, 2024 -
coq-simple-io Public
Forked from Lysxia/coq-simple-ioIO for Gallina
Coq MIT License UpdatedSep 19, 2024 -
cross-crypto Public
Forked from mit-plv/cross-cryptoConnecting computational and symbolic crypto models
Coq MIT License UpdatedSep 18, 2024 -
engine-bench Public
Forked from mit-plv/engine-benchBenchmarks for various proof engines
Coq MIT License UpdatedSep 18, 2024 -
category-theory Public
Forked from jwiegley/category-theoryAn axiom-free formalization of category theory in Coq for personal study and practical work
Coq BSD 3-Clause "New" or "Revised" License UpdatedSep 18, 2024 -
neural-net-coq-interp Public
Forked from JasonGross/neural-net-coq-interpSome experiments with doing NN interpretability in Coq
Jupyter Notebook MIT License UpdatedSep 18, 2024 -
Coqtail Public
Forked from whonore/CoqtailInteractive Coq Proofs in Vim
Python MIT License UpdatedSep 17, 2024 -
rupicola Public
Forked from mit-plv/rupicolaExtracting imperative code from Gallina
Coq MIT License UpdatedSep 17, 2024 -
bedrock2 Public
Forked from mit-plv/bedrock2A work-in-progress language and compiler for verified low-level programming
Coq MIT License UpdatedSep 17, 2024