Skip to content
@rocq-archive

The Rocq Prover Archive

This organization is used to archive unmaintained projects related to the Coq / Rocq Prover ecosystem, including, but not limited to, former "Coq contribs".

The Rocq Prover Archive

This organization is used to archive unmaintained projects related to the Coq / Rocq Prover ecosystem, including, but not limited to, former "Coq contribs".

While projects in this archive are (virtually) unmaintained, any project can be picked up and maintained again if there is interest.

If you volunteer to become the new maintainer of a project in the Archive, please signal your interest in an issue of the Coq-community manifesto repository (either a new issue, or an existing one if an issue has already been opened to note that the project is looking for a new maintainer): https://github.com/coq-community/manifesto/

Authors of unmaintained Rocq Prover related projects are also welcome to propose their projects for adoption in the Coq-community manifesto issue tracker. In case a volunteer is found, the project can be transfered directly in Coq-community, but in case no volunteer is found, they can be transfered to the Rocq Prover Archive until someone is eventually interested in picking up the project.

This Archive is co-managed by Coq / Rocq core developers and Coq-community admins.

Popular repositories Loading

  1. coq-serapi coq-serapi Public

    Coq Protocol Playground with Se(xp)rialization of Internal Structures.

    Coq 128 39

  2. coq-in-coq coq-in-coq Public

    A formalisation of the Calculus of Constructions

    Coq 66 7

  3. automata automata Public

    Beginning of formal language theory

    Coq 23 2

  4. zfc zfc Public

    An encoding of Zermelo-Fraenkel Set Theory in Coq

    Coq 22 3

  5. ltl ltl Public

    Linear Temporal Logic

    Coq 19 5

  6. group-theory group-theory Public

    Elements of Group Theory

    Coq 14 1

Repositories

Showing 10 of 150 repositories
  • .github Public
    rocq-archive/.github’s past year of commit activity
    0 0 0 0 Updated Nov 13, 2024
  • coq-serapi Public

    Coq Protocol Playground with Se(xp)rialization of Internal Structures.

    rocq-archive/coq-serapi’s past year of commit activity
    Coq 128 39 0 3 Updated Nov 13, 2024
  • paradoxes Public

    Paradoxes in Set Theory and Type Theory

    rocq-archive/paradoxes’s past year of commit activity
    Coq 11 LGPL-2.1 0 0 0 Updated Jul 24, 2024
  • coq-in-coq Public

    A formalisation of the Calculus of Constructions

    rocq-archive/coq-in-coq’s past year of commit activity
    Coq 66 LGPL-2.1 7 0 0 Updated Jul 24, 2024
  • lambek Public

    A Coq Toolkit for Lambek Calculus

    rocq-archive/lambek’s past year of commit activity
    Coq 7 LGPL-2.1 1 0 0 Updated Jul 24, 2024
  • ltl Public

    Linear Temporal Logic

    rocq-archive/ltl’s past year of commit activity
    Coq 19 5 0 0 Updated Jan 9, 2024
  • ipc Public

    Intuitionistic Propositional Checker

    rocq-archive/ipc’s past year of commit activity
    Coq 4 2 0 0 Updated Feb 10, 2023
  • zfc Public

    An encoding of Zermelo-Fraenkel Set Theory in Coq

    rocq-archive/zfc’s past year of commit activity
    Coq 22 LGPL-2.1 3 5 1 Updated Dec 17, 2022
  • rocq-archive/coq-contribs’s past year of commit activity
    OCaml 7 1 2 0 Updated May 19, 2021
  • zchinese Public

    A proof of the Chinese Remainder Lemma

    rocq-archive/zchinese’s past year of commit activity
    Coq 1 1 0 1 Updated Oct 28, 2020

People

This organization has no public members. You must be a member to see who’s a part of this organization.

Top languages

Loading…

Most used topics

Loading…