Topic: "paper-artifacts"
rocq-community/lemma-overloading
Libraries demonstrating design patterns for programming and proving with canonical structures in Coq [maintainer=@anton-trunov]
Language: Coq - Size: 1.1 MB - Last synced at: about 1 month ago - Pushed at: about 1 month ago - Stars: 27 - Forks: 6
rocq-community/alea
Coq library for reasoning on randomized algorithms [maintainers=@anton-trunov,@volodeyka]
Language: Coq - Size: 139 KB - Last synced at: 29 days ago - Pushed at: over 3 years ago - Stars: 25 - Forks: 0
rocq-community/bits
A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]
Language: Coq - Size: 188 KB - Last synced at: 29 days ago - Pushed at: 3 months ago - Stars: 23 - Forks: 7
rocq-community/qarith-stern-brocot
Binary rational numbers in Coq [maintainer=@herbelin]
Language: Coq - Size: 394 KB - Last synced at: 29 days ago - Pushed at: over 1 year ago - Stars: 14 - Forks: 4
rocq-community/almost-full
Coq development of almost-full relations, including the Ramsey Theorem, useful for proving termination [maintainer=@palmskog]
Language: Coq - Size: 1.47 MB - Last synced at: about 2 months ago - Pushed at: over 1 year ago - Stars: 3 - Forks: 0
cogumbreiro/gorn-coq
Deadlock avoidance on using futures in shared memory. The project includes the formalization of a trace language and results on a policy on safe joins (through a notion of known tasks) and we show that data-race-freedom implies deadlock freedom.
Language: Coq - Size: 421 KB - Last synced at: about 2 years ago - Pushed at: over 7 years ago - Stars: 0 - Forks: 2
