Skip to content

@rocq-archive The Rocq Prover Archive

Change the repository type filter

All

    Repositories list

    151 repositories

    • sum-of-two-square

      Public
      Numbers equal to the sum of two square numbers
      Rocq Prover
      •
      GNU Lesser General Public License v2.1
      •2•2•0•0•Updated Jan 30, 2026Jan 30, 2026

    • coq-serapi

      Public
      Coq Protocol Playground with Se(xp)rialization of Internal Structures.
      serializationjsonprotocolcoqproof-assistantsexpmachine-learning-api
      Coq
      •
      Other
      •41•137•2•0•Updated Nov 27, 2025Nov 27, 2025

    • tarski-geometry

      Public archive
      Tarski's geometry - archived since the formalization is now maintained as part of GeoCoq
      Coq
      •1•2•0•0•Updated May 13, 2025May 13, 2025

    • .github

      Public
      0•0•0•0•Updated May 9, 2025May 9, 2025

    • paradoxes

      Public
      Paradoxes in Set Theory and Type Theory
      Coq
      •
      GNU Lesser General Public License v2.1
      •0•12•0•0•Updated Jul 24, 2024Jul 24, 2024

    • coq-in-coq

      Public
      A formalisation of the Calculus of Constructions
      Coq
      •
      GNU Lesser General Public License v2.1
      •8•70•0•0•Updated Jul 24, 2024Jul 24, 2024

    • lambek

      Public
      A Coq Toolkit for Lambek Calculus
      Coq
      •
      GNU Lesser General Public License v2.1
      •0•7•0•0•Updated Jul 24, 2024Jul 24, 2024

    • stdlib2

      Public
      Coq
      •
      GNU Lesser General Public License v2.1
      •9•37•14•0•Updated Jan 17, 2024Jan 17, 2024

    • ltl

      Public
      Linear Temporal Logic
      Coq
      •5•21•0•0•Updated Jan 9, 2024Jan 9, 2024

    • ipc

      Public
      Intuitionistic Propositional Checker
      Coq
      •2•5•0•0•Updated Feb 10, 2023Feb 10, 2023

    • zfc

      Public
      An encoding of Zermelo-Fraenkel Set Theory in Coq
      Coq
      •
      GNU Lesser General Public License v2.1
      •3•24•5•1•Updated Dec 17, 2022Dec 17, 2022

    • coq-contribs

      Public
      OCaml
      •1•7•2•0•Updated May 19, 2021May 19, 2021

    • zchinese

      Public
      A proof of the Chinese Remainder Lemma
      Coq
      •1•1•0•1•Updated Oct 28, 2020Oct 28, 2020

    • zsearch-trees

      Public
      Binary Search Trees
      Coq
      •
      GNU Lesser General Public License v2.1
      •1•0•0•0•Updated Oct 18, 2020Oct 18, 2020

    • zf

      Public
      An axiomatisation of intuitionistic Zermelo-Fraenkel set theory
      Coq
      •1•0•0•0•Updated Oct 18, 2020Oct 18, 2020

    • weak-up-to

      Public
      New Up-to Techniques for Weak Bisimulation
      Coq
      •
      Other
      •0•3•0•0•Updated Oct 18, 2020Oct 18, 2020

    • traversable-fincontainer

      Public
      Traversable Functors are Finitary Containers
      Coq
      •0•0•0•0•Updated Oct 18, 2020Oct 18, 2020

    • subst

      Public
      The confluence of Hardin-Lévy lambda-sigma-lift-calcul
      Coq
      •0•0•0•0•Updated Oct 18, 2020Oct 18, 2020

    • streams

      Public
      Specification of Eratosthene Sieve
      Coq
      •
      GNU Lesser General Public License v2.1
      •0•1•0•0•Updated Oct 18, 2020Oct 18, 2020

    • shuffle

      Public
      Gilbreath's card trick
      Coq
      •
      GNU Lesser General Public License v2.1
      •0•0•0•0•Updated Oct 18, 2020Oct 18, 2020

    • search-trees

      Public
      Binary Search Trees
      Coq
      •
      GNU Lesser General Public License v2.1
      •0•0•0•0•Updated Oct 18, 2020Oct 18, 2020

    • schroeder

      Public
      The Theorem of Schroeder-Bernstein
      Coq
      •
      GNU Lesser General Public License v2.1
      •0•0•0•0•Updated Oct 18, 2020Oct 18, 2020

    • rsa

      Public
      Correctness of RSA algorithm
      Coq
      •
      GNU Lesser General Public License v2.1
      •0•3•0•0•Updated Oct 18, 2020Oct 18, 2020

    • rem

      Public
      Rem Theorem in Baire space
      Coq
      •
      GNU Lesser General Public License v2.1
      •0•0•0•0•Updated Oct 18, 2020Oct 18, 2020

    • reflexive-first-order

      Public
      Reflexive first-order proof interpreter
      Coq
      •0•0•0•0•Updated Oct 18, 2020Oct 18, 2020

    • ramsey

      Public
      Ramsey Theory
      Coq
      •
      GNU Lesser General Public License v2.1
      •0•2•0•0•Updated Oct 18, 2020Oct 18, 2020

    • ptsatr

      Public
      Formalization of the proof that PTS and PTS with judgmental equality (PTSe) are equivalent. With this equivalence, we are able to derive all the meta-theory of …
      Coq
      •0•2•0•0•Updated Oct 18, 2020Oct 18, 2020

    • prfx

      Public
      Proof Reflection in Coq
      Coq
      •0•0•0•0•Updated Oct 18, 2020Oct 18, 2020

    • pi-calc

      Public
      Pi-calculus in Coq
      Coq
      •1•10•0•0•Updated Oct 18, 2020Oct 18, 2020

    • param-pi

      Public
      Coding of a typed monadic pi-calculus using parameters for free names
      Coq
      •
      GNU Lesser General Public License v2.1
      •0•2•0•0•Updated Oct 18, 2020Oct 18, 2020