Rocq
Showing 21 of 21 projects
A Coq library formalizing mathematics using univalent foundations and homotopy type theory.
An extensive and coherent library of formalized mathematical theories built on the Coq/Rocq proof assistant with SSReflect.
A project formalizing the Rocq proof assistant in Rocq itself, providing tools for metaprogramming and developing certified plugins.
A Visual Studio Code extension providing language server support for the Rocq/Coq interactive theorem prover.
A Visual Studio Code extension providing language server support for the Rocq/Coq interactive theorem prover.
Translates OCaml programs to Coq for formal verification of properties like invariants and absence of failures.
Translates OCaml programs to Coq for formal verification of properties like invariants, absence of failures, and backward compatibility.
A formal real analysis library for the Coq/Rocq proof assistant, built on the Mathematical Components library.
An automated reasoning hammer tool for Rocq that combines learning with external provers to automate proofs in dependent type theory.
A function definition plugin for Rocq/Coq that provides notation for dependent pattern-matching and well-founded recursion.
A language server and VS Code extension providing incremental checking, error recovery, and IDE features for the Rocq/Coq proof assistant.
A Coq framework for formal verification, property-based testing, and extraction of smart contracts.
A textbook on modeling and proving in computational type theory using the Rocq proof assistant.
A Rocq library for formal reasoning about discrete probabilities, information theory, and linear error-correcting codes.
A Rocq library providing a formalized hierarchy of monads and their laws for monadic equational reasoning.
A collaborative, community-driven organization for the long-term maintenance and promotion of packages for the Rocq Prover.
A modular relation algebra library for Rocq (Coq) with reflexive decision tactics for Kleene algebra with tests and related theories.
Provides ring, field, lra, nra, and psatz tactics for the Mathematical Components library in Coq.
A Rocq/Coq library providing formal definitions and mechanically verified proofs for rewriting theory, λ-calculus, and termination analysis.
Extends Coq's zify tactic to support Mathematical Components library definitions for arithmetic solving.
A Rocq library providing stable mergesort algorithms with formal correctness proofs using relational parametricity.
Related Tags
Found a gem we're missing?
Open-Awesome is built by the community, for the community. Submit a project, suggest an awesome list, or help improve the catalog on GitHub.