-
ONERA
- Toulouse
-
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…
-
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 UpdatedSep 13, 2024 -
nixpkgs Public
Forked from NixOS/nixpkgsNix Packages collection & NixOS
Nix MIT License UpdatedSep 13, 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 UpdatedSep 13, 2024 -
-
Coqtail Public
Forked from whonore/CoqtailInteractive Coq Proofs in Vim
Python MIT License UpdatedSep 13, 2024 -
metacoq Public
Forked from MetaCoq/metacoqMetaprogramming in Coq
Coq MIT License UpdatedSep 13, 2024 -
CompCert Public
Forked from AbsInt/CompCertThe CompCert formally-verified C compiler
Coq Other UpdatedSep 13, 2024 -
coq-elpi Public
Forked from LPCIC/coq-elpiCoq plugin embedding elpi
OCaml GNU Lesser General Public License v2.1 UpdatedSep 11, 2024 -
fiat-crypto Public
Forked from mit-plv/fiat-cryptoCryptographic Primitive Code Generation by Fiat
Coq Other UpdatedSep 11, 2024 -
VST Public
Forked from PrincetonUniversity/VSTVerified Software Toolchain
Coq Other UpdatedSep 11, 2024 -
perennial Public
Forked from mit-pdos/perennialVerifying concurrent crash-safe systems
Coq MIT License UpdatedSep 11, 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 UpdatedSep 10, 2024 -
coq-serapi Public
Forked from ejgallego/coq-serapiCoq Protocol Playground with Se(xp)rialization of Internal Structures.
OCaml Other UpdatedSep 10, 2024 -
coq.github.io Public
Forked from coq/coq.github.ioSource files of the coq.inria.fr website
HTML Other UpdatedSep 10, 2024 -
QuickChick Public
Forked from QuickChick/QuickChickRandomized Property-Based Testing Plugin for Coq
Coq Other UpdatedSep 10, 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 UpdatedSep 6, 2024 -
opam-repository Public
Forked from ocaml/opam-repositoryMain public package repository for OPAM, the source package manager of OCaml.
-
coq-waterproof Public
Forked from impermeable/coq-waterproofCoq GNU Lesser General Public License v3.0 UpdatedSep 3, 2024 -
-
coq-simple-io Public
Forked from Lysxia/coq-simple-ioIO for Gallina
Coq MIT License UpdatedSep 3, 2024 -
-
rupicola Public
Forked from mit-plv/rupicolaExtracting imperative code from Gallina
Coq MIT License UpdatedSep 3, 2024 -
riscv-coq Public
Forked from mit-plv/riscv-coqRISC-V Specification in Coq
Coq BSD 3-Clause "New" or "Revised" License UpdatedSep 3, 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 3, 2024 -
-
InteractionTrees Public
Forked from DeepSpec/InteractionTreesA Library for Representing Recursive and Impure Programs in Coq
Coq MIT License UpdatedSep 3, 2024 -
engine-bench Public
Forked from mit-plv/engine-benchBenchmarks for various proof engines
Coq MIT License UpdatedSep 3, 2024 -
coqutil Public
Forked from mit-plv/coqutilCoq library for tactics, basic definitions, sets, maps
Coq MIT License UpdatedSep 3, 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 3, 2024