Rocq-community
Pinned Loading
Repositories
- tarjan Public
Coq formalization of algorithms due to Tarjan and Kosaraju for finding strongly connected graph components using Mathematical Components and SSReflect [maintainers=@CohenCyril,@palmskog]
rocq-community/tarjan’s past year of commit activity - bits Public
A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]
rocq-community/bits’s past year of commit activity - apery Public
A formal proof of the irrationality of zeta(3), the Apéry constant [maintainer=@amahboubi,@pi8027]
rocq-community/apery’s past year of commit activity - docker-rocq Public
Docker images of the Rocq Prover (see also: https://github.com/rocq-community/docker-coq-action) [maintainer=@Justme0606]
rocq-community/docker-rocq’s past year of commit activity - rocq-program-verification-template Public template
Template project for program verification in the Rocq Prover, showcasing reasoning on CompCert's Clight language using the Verified Software Toolchain [maintainer=@palmskog]
rocq-community/rocq-program-verification-template’s past year of commit activity
Top languages
Loading…
Most used topics
Loading…