Programming Language Theory Concept

Rocq kernel

Books

Journey Statuslearning Tags

Tools: Rocq (formerly Coq)

(Compiler implementation) The trusted core of Rocq that type-checks proof terms against the Calculus of Inductive Constructions, ensuring all accepted proofs are valid.