GitHub topics: docker-coq-action
rocq-community/huffman
Correctness proof of the Huffman coding algorithm in Coq [maintainer=@palmskog]
Language: Rocq Prover - Size: 1.02 MB - Last synced at: about 24 hours ago - Pushed at: 1 day ago - Stars: 14 - Forks: 4
rocq-community/aac-tactics
Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainer=@palmskog]
Language: OCaml - Size: 648 KB - Last synced at: 4 days ago - Pushed at: 4 days ago - Stars: 34 - Forks: 24
rocq-community/bignums
Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library [maintainers=@proux01,@erikmd]
Language: Rocq Prover - Size: 823 KB - Last synced at: 12 days ago - Pushed at: 12 days ago - Stars: 25 - Forks: 23
rocq-community/paramcoq
Old Coq plugin for parametricity [maintainer=@ppedrot]
Language: Rocq Prover - Size: 563 KB - Last synced at: 16 days ago - Pushed at: 17 days ago - Stars: 45 - Forks: 27
rocq-community/coq-dpdgraph
Build dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]
Language: Rocq Prover - Size: 378 KB - Last synced at: 27 days ago - Pushed at: about 2 months ago - Stars: 93 - Forks: 32
rocq-community/graph-theory
Graph Theory [maintainers=@chdoc,@damien-pous]
Language: Rocq Prover - Size: 4.65 MB - Last synced at: 2 days ago - Pushed at: 2 days ago - Stars: 39 - Forks: 4
rocq-community/docker-coq-action
GitHub Action using Docker-Coq [maintainers=@erikmd,@Zimmi48]
Language: Shell - Size: 275 KB - Last synced at: 7 days ago - Pushed at: 7 months ago - Stars: 14 - Forks: 5
ProofGeneral/PG
This repo is the new home of Proof General
Language: Emacs Lisp - Size: 26.6 MB - Last synced at: 3 months ago - Pushed at: 3 months ago - Stars: 530 - Forks: 94
rocq-community/gaia
Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]
Language: Rocq Prover - Size: 2.2 MB - Last synced at: 4 months ago - Pushed at: 4 months ago - Stars: 30 - Forks: 7
rocq-community/coq-art
Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]
Language: Coq - Size: 545 KB - Last synced at: 5 months ago - Pushed at: 9 months ago - Stars: 120 - Forks: 24
rocq-community/stalmarck
Certified implementation in Coq of Stålmarck's algorithm for proving tautologies [maintainer=@palmskog]
Language: Coq - Size: 374 KB - Last synced at: 4 months ago - Pushed at: about 1 year ago - Stars: 2 - Forks: 4
rocq-community/reglang
Regular Language Representations in Coq [maintainers=@chdoc,@palmskog]
Language: Coq - Size: 552 KB - Last synced at: 5 months ago - Pushed at: 6 months ago - Stars: 43 - Forks: 7
rocq-community/hydra-battles
Variations on Kirby & Paris' hydra battles and other entertaining math in Coq (collaborative, documented, includes exercises) [maintainer=@Casteran]
Language: Coq - Size: 20.9 MB - Last synced at: 5 months ago - Pushed at: 9 months ago - Stars: 75 - Forks: 12
rocq-community/buchberger
Verified implementation in Coq of Buchberger's algorithm for computing Gröbner bases [maintainer=@palmskog]
Language: Coq - Size: 272 KB - Last synced at: 4 months ago - Pushed at: almost 2 years ago - Stars: 10 - Forks: 1
rocq-community/mmaps
Modular Finite Maps over Ordered Types in Coq [maintainers=@letouzey,@palmskog]
Language: Coq - Size: 734 KB - Last synced at: 5 months ago - Pushed at: over 1 year ago - Stars: 12 - Forks: 3
rocq-community/goedel 📦
Archived since the contents have been moved to the Hydras & Co. repository
Language: Coq - Size: 542 KB - Last synced at: 5 months ago - Pushed at: about 3 years ago - Stars: 29 - Forks: 5
rocq-community/qarith-stern-brocot
Binary rational numbers in Coq [maintainer=@herbelin]
Language: Coq - Size: 394 KB - Last synced at: 4 months ago - Pushed at: almost 2 years ago - Stars: 14 - Forks: 4
rocq-community/jmlcoq
Coq definition of JML and a verified runtime assertion checker [maintainer=@palmskog]
Language: Coq - Size: 430 KB - Last synced at: 7 months ago - Pushed at: almost 2 years ago - Stars: 4 - Forks: 0
rocq-community/regexp-Brzozowski
Coq formalization of decision procedures for regular expression equivalence [maintainer=@anton-trunov]
Language: Coq - Size: 254 KB - Last synced at: 4 months ago - Pushed at: over 1 year ago - Stars: 13 - Forks: 1
rocq-community/chapar
A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]
Language: Coq - Size: 1.94 MB - Last synced at: 4 months ago - Pushed at: almost 2 years ago - Stars: 32 - Forks: 7
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: 4 months ago - Pushed at: almost 2 years ago - Stars: 3 - Forks: 0
rocq-community/pocklington
Pocklington's criterion for primality in Coq [maintainer=@Casteran]
Language: Coq - Size: 96.7 KB - Last synced at: 7 months ago - Pushed at: over 3 years ago - Stars: 2 - Forks: 0