-
Goeland Public
Forked from GoelandProver/GoelandA first-order concurrent automated theorem prover
-
rocq Public
Forked from rocq-prover/rocqThe Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environmen…
OCaml GNU Lesser General Public License v2.1 UpdatedOct 22, 2025 -
rocq-lsp Public
Forked from ejgallego/rocq-lspVisual Studio Code Extension and Language Server Protocol for Coq
OCaml GNU Lesser General Public License v2.1 UpdatedOct 14, 2025 -
Rocq-Equations Public
Forked from mattam82/Coq-EquationsA function definition package for Coq
Coq GNU Lesser General Public License v2.1 UpdatedSep 25, 2025 -
metarocq Public
Forked from MetaRocq/metarocqMetaprogramming, verified meta-theory and implementation of Rocq in Rocq
Coq MIT License UpdatedJul 24, 2025 -
rocq-rfcs Public
Forked from rocq-prover/rfcsRocq RFCs: documents to discuss changes to the Rocq Prover
UpdatedJul 18, 2025 -
Supplementary material for the report of my Master 2 internship
Rocq Prover UpdatedJun 26, 2025 -
rocq-elpi Public
Forked from LPCIC/coq-elpiCoq plugin embedding elpi
Coq GNU Lesser General Public License v2.1 UpdatedApr 11, 2025 -
rocq-tactician Public
Forked from coq-tactician/coq-tacticianA Seamless, Interactive Tactic Learner and Prover for Coq
OCaml MIT License UpdatedApr 11, 2025 -
rocq-stdlib Public
Forked from rocq-prover/stdlibStdlib for the Rocq Prover
Coq GNU Lesser General Public License v2.1 UpdatedApr 11, 2025 -
unicoq Public
Forked from unicoq/unicoqAn enhanced unification algorithm for Coq
OCaml MIT License UpdatedApr 11, 2025 -
rocqhammer Public
Forked from lukaszcz/coqhammerCoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
OCaml Other UpdatedApr 7, 2025 -
rewriter Public
Forked from mit-plv/rewriterReflective PHOAS rewriting/pattern-matching-compilation framework for simply-typed equalities and let-lifting
Coq Other UpdatedApr 3, 2025 -
advent-of-code Public
Solutions for the Advent of Code (since 2020)
C++ Creative Commons Zero v1.0 Universal UpdatedDec 27, 2024 -
poset-type-theory Public
Forked from JonasHoefer/poset-type-theoryExperimental implementation of a Cubical Type Theory modeled by presheaves over posets
Haskell MIT License UpdatedAug 2, 2024 -
Homotopy-Finiteness Public
A formalisation of the homotopy finiteness proof in Jonas Hoefer's prototype, and some applications.
-
A minimal GitHub action to export org-mode files to HTML and publish it as a GitHub page.
Emacs Lisp UpdatedJul 10, 2024 -
ModuleDiffing Public
This directory aims towards giving better error messages for OCaml modules through tree diffing algorithms.
OCaml UpdatedMar 17, 2024 -
Survival-Horror-Game Public archive
Repository for Hello World's second online game jam.
ASP UpdatedNov 23, 2019
{{ message }}