Rocq-community
Change the repository type filter
All
Repositories list
77 repositories
coqeal
PublicThe Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]graph-theory
PublicGraph Theory [maintainers=@chdoc,@damien-pous]coq-nix-toolbox
Publicatbr
PublicCoq library and tactic for deciding Kleene algebras [maintainer=@tchajed]- A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]
aac-tactics
PublicCoq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainer=@palmskog]- Visual Studio Code Extension and Language Server Protocol for Rocq / Coq [maintainers=@gbdrt,@SkySkimmer,@tabareau]
micromega-plugin
Public- Build dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]
coqtail-math
PublicCoqtail is a library of mathematical theorems and tools proved inside the Coq proof assistant. Results range mostly from arithmetic to real and complex analysis…trocq
PublicA modular parametricity plugin for proof transfer in Coq [maintainers=@CohenCyril,@ecranceMERCE,@amahboubi,@lweqx,@MysaaJava]parseque
PublicTotal Parser Combinators in Coq [maintainer=@womeier]rocq-lean-import
Publiccorn
PublicCoq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]docker-rocq
Publicrun-coq-bug-minimizer
Publicstalmarck
PublicCertified implementation in Coq of Stålmarck's algorithm for proving tautologies [maintainer=@palmskog]fourcolor
Publicparamcoq
PublicOld Coq plugin for parametricity [maintainer=@ppedrot]bignums
PublicCoq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library [maintainers=@proux01,@erikmd]docker-base
PublicParent image for Docker images of the Coq proof assistant [maintainer=@Justme0606]templates
PublicTemplates for configuration files and scripts useful for maintaining Coq projects [maintainers=@liyishuai,@palmskog,@Zimmi48]reglang
PublicRegular Language Representations in Coq [maintainers=@chdoc,@palmskog]tarjan
PublicCoq formalization of algorithms due to Tarjan and Kosaraju for finding strongly connected graph components using Mathematical Components and SSReflect [maintain…gaia
PublicImplementation of books from Bourbaki's Elements of Mathematics in Coq [maintainer=@thery]bits
PublicA formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]apery
Publicrocq-program-verification-template
Public templateTemplate project for program verification in the Rocq Prover, showcasing reasoning on CompCert's Clight language using the Verified Software Toolchain [maintain…lemma-overloading
PublicLibraries demonstrating design patterns for programming and proving with canonical structures in Coq [maintainer=@anton-trunov]semantics
PublicA survey of semantics styles in Coq, from natural semantics through structural operational, axiomatic, and denotational semantics, to abstract interpretation [m…
ProTip! When viewing an organization's repositories, you can use the
props. filter to filter by custom property.