Repositories list

• metarocq

  Public
  Metaprogramming, verified meta-theory and implementation of Rocq in Rocq

  metaprogrammingcoqcoq-formalization+ 1rocq

  Rocq Prover

  •

  MIT License

  •94•486•63•32•Updated Dec 5, 2025Dec 5, 2025

• nested-eliminators

  Public
  Derivation of sparse parametricity and nested eliminators

  Rocq Prover

  •

  MIT License

  •1•1•0•0•Updated Nov 15, 2025Nov 15, 2025

• metarocq.github.io

  Public
  Website of the MetaRocq Project

  HTML

  •

  MIT License

  •0•2•1•0•Updated Sep 16, 2025Sep 16, 2025

• rocq-verified-extraction

  Public
  Verified Extraction from Rocq to OCaml/Malfunction

  Coq

  •

  MIT License

  •5•13•0•1•Updated May 23, 2025May 23, 2025

• tutorials

  Public
  Coq

  •

  MIT License

  •0•4•0•0•Updated Dec 13, 2024Dec 13, 2024