MetaRocq

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

MetaRocq/metarocq’s past year of commit activity

Rocq Prover 497 MIT 96 62 (1 issue needs help) 30 Updated Jan 13, 2026
nested-eliminators Public
Derivation of sparse parametricity and nested eliminators

MetaRocq/nested-eliminators’s past year of commit activity

Rocq Prover 1 MIT 1 0 0 Updated Nov 15, 2025
metarocq.github.io Public
Website of the MetaRocq Project

MetaRocq/metarocq.github.io’s past year of commit activity

HTML 2 MIT 0 1 0 Updated Sep 16, 2025
rocq-verified-extraction Public
Verified Extraction from Rocq to OCaml/Malfunction

MetaRocq/rocq-verified-extraction’s past year of commit activity

Coq 14 MIT 5 0 1 Updated May 23, 2025
tutorials Public

MetaRocq/tutorials’s past year of commit activity

Coq 4 MIT 0 0 0 Updated Dec 13, 2024

Provide feedback