-
coq-elpi Public
Forked from LPCIC/coq-elpiCoq plugin embedding elpi
Prolog GNU Lesser General Public License v2.1 UpdatedFeb 10, 2025 -
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…
-
A Visual Studio Code extension for Coq [maintainers=@maximedenes,@fakusb]
TypeScript MIT License UpdatedFeb 4, 2025 -
coq-lsp Public
Forked from ejgallego/coq-lspLanguage Server Protocol and VS Code Extension for Coq
OCaml GNU Lesser General Public License v2.1 UpdatedFeb 3, 2025 -
metacoq Public
Forked from MetaCoq/metacoqMetaprogramming in Coq
Coq MIT License UpdatedFeb 1, 2025 -
logrel-coq Public
Forked from CoqHott/logrel-coqLogical Relation for MLTT in Coq
Coq UpdatedJan 31, 2025 -
CompCert Public
Forked from AbsInt/CompCertThe CompCert formally-verified C compiler
Coq Other UpdatedJan 16, 2025 -
paramcoq Public
Forked from coq-community/paramcoqCoq plugin for parametricity [maintainer=@proux01]
Coq Other UpdatedJan 15, 2025 -
coq-scripts Public
Forked from JasonGross/coq-scriptsVarious useful scripts for dealing with Coq files
Coq MIT License UpdatedJan 15, 2025 -
opam-coq-archive Public
Forked from coq/opamArchive for all Coq related OPAM packages organized in various repositories
-
-
-
malfunction Public
Forked from stedolan/malfunctionMalfunctional Programming
OCaml Other UpdatedDec 10, 2024 -
coq-waterproof Public
Forked from impermeable/coq-waterproofThe Waterproof plugin for the Coq proof assistant allows you to write Coq proofs in a style that resembles handwritten mathematical proofs, designed to help university students with learning how to…
Coq GNU Lesser General Public License v3.0 UpdatedNov 13, 2024 -
relation-algebra Public
Forked from damien-pous/relation-algebraRelation algebra library for Coq
-
coq-tactician Public
Forked from coq-tactician/coq-tacticianA Seamless, Interactive Tactic Learner and Prover for Coq
OCaml MIT License UpdatedOct 23, 2024 -
coq-serapi Public
Forked from rocq-archive/coq-serapiCoq Protocol Playground with Se(xp)rialization of Internal Structures.
OCaml Other UpdatedOct 22, 2024 -
atbr Public
Forked from coq-community/atbrCoq library and tactic for deciding Kleene algebras [maintainer=@tchajed]
Coq Other UpdatedOct 21, 2024 -
-
ll-coq Public
Some Coq formalizations of Linear Logic
-
-
VST Public
Forked from PrincetonUniversity/VSTVerified Software Toolchain
Coq Other UpdatedAug 9, 2024 -
category-theory Public
Forked from jwiegley/category-theoryAn axiom-free formalization of category theory in Coq for personal study and practical work
-
elpi Public
Forked from LPCIC/elpiEmbeddable Lambda Prolog Interpreter
Prolog GNU Lesser General Public License v2.1 UpdatedJul 30, 2024 -
fiat-crypto Public
Forked from mit-plv/fiat-cryptoCryptographic Primitive Code Generation by Fiat
Coq MIT License UpdatedJul 29, 2024 -
neural-net-coq-interp Public
Forked from JasonGross/neural-net-coq-interpSome experiments with doing NN interpretability in Coq
Jupyter Notebook MIT License UpdatedJul 27, 2024 -
Coq-Equations Public
Forked from mattam82/Coq-EquationsA plugin for Coq to add dependent pattern-matching.
OCaml GNU Lesser General Public License v2.1 UpdatedJul 23, 2024 -
smtcoq Public
Forked from smtcoq/smtcoqCommunication between Coq and SAT/SMT solvers
OCaml Other UpdatedJun 3, 2024 -
quote-mltt-lics24 Public
Companion development of the LICS'24 paper “Upon This Quote I Will Build My Church Thesis”
Coq UpdatedMay 17, 2024 -
QuickChick Public
Forked from QuickChick/QuickChickRandomized Property-Based Testing Plugin for Coq
Coq Other UpdatedMay 5, 2024
{{ message }}