docker-coq-action 开源项目推荐（22 个）

ProofGeneral /PG

This repo is the new home of Proof General

rocq-community /coq-art

Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]

rocq-community /coq-dpdgraph

Build dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]

rocq-community /hydra-battles

Kirby和Paris的Hydra战斗和Coq中其他有趣数学的变体（协作、记录、包括练习）[maintainer=@Casteran]

rocq-community /reglang

Regular Language Representations in Coq [maintainers=@chdoc,@palmskog]

rocq-community /graph-theory

Graph Theory [maintainers=@chdoc,@damien-pous]

rocq-community /paramcoq

Old Coq plugin for parametricity [maintainer=@ppedrot]

rocq-community /aac-tactics

Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainer=@palmskog]

rocq-community /chapar

A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]

rocq-community /gaia

Implementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]

rocq-community /goedel

Archived since the contents have been moved to the Hydras & Co. repository

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]

rocq-prover /docker-opam-action

GitHub Action using Docker-Coq [maintainers=@Justme0606,@Zimmi48]

rocq-community /qarith-stern-brocot

Binary rational numbers in Coq [maintainer=@herbelin]

rocq-community /regexp-Brzozowski

Coq formalization of decision procedures for regular expression equivalence [maintainer=@anton-trunov]

rocq-community /huffman

Correctness proof of the Huffman coding algorithm in Coq [maintainer=@palmskog]

rocq-community /mmaps

Modular Finite Maps over Ordered Types in Coq [maintainers=@letouzey,@palmskog]

rocq-community /buchberger

Verified implementation in Coq of Buchberger's algorithm for computing Gröbner bases [maintainer=@palmskog]

rocq-community /jmlcoq

Coq definition of JML and a verified runtime assertion checker [maintainer=@palmskog]

rocq-community /almost-full

Coq development of almost-full relations, including the Ramsey Theorem, useful for proving termination [maintainer=@palmskog]