Stars
Minimal implementations for dependent type checking and elaboration
Enter Unicode characters using LaTeX notation
Documentation on goals of the Rocq-community organization, the shared contributing guide and code of conduct.
"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.
This repo is the new home of Proof General
A Redex model of CIC as specified in Chapter 4 of the Coq reference manual.
A plugin for Coq that implements the call-by-name forcing translation
A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]
Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]
🍻 Default formulae for the missing package manager for macOS (or Linux)
🍺 The missing package manager for macOS (or Linux)
Research prototype tool for modular formal verification of C, Rust and Java programs
The core OCaml system: compilers, runtime system, base libraries
The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environmen…
Archive for all Rocq and Coq-related opam packages organized in various repositories