coq-ecosystem
What are the most popular libraries in the Coq ecosystem?
| Number | Name | Description | Stars |
|---|---|---|---|
| 1 | coq/coq | Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. | 1584 |
| 2 | HoTT/HoTT | Homotopy type theory | 619 |
| 3 | AbsInt/CompCert | The CompCert formally-verified C compiler | 582 |
| 4 | UniMath/UniMath | This coq library aims to formalize a substantial body of mathematics using the univalent point of view. | 423 |
| 5 | uwplse/verdi | A framework for formally verifying distributed systems implementations in Coq | 392 |
| 6 | jwiegley/category-theory | An axiom-free formalization of category theory in Coq for personal study and practical work | 380 |
| 7 | achlipala/frap | Formal Reasoning About Programs | 259 |
| 8 | antalsz/hs-to-coq | Convert Haskell source code to Coq source code | 195 |
| 9 | UniMath/Foundations | Voevodsky's original development of the univalent foundations of mathematics in Coq | 193 |
| 10 | math-comp/math-comp | Mathematical Components | 172 |
| 11 | jscert/jscert | A Coq specification of ECMAScript 5 (JavaScript) with verified reference interpreter | 165 |
| 12 | pirapira/coq2rust | Coq to Rust program extraction. The whole tree is on the original Coq code base. | 161 |
| 13 | mit-pdos/fscq | FSCQ is a certified file system written and proven in Coq | 154 |
| 14 | clarus/coq-chick-blog | A blog engine written and proven in Coq. | 143 |
| 15 | PrincetonUniversity/VST | Verified Software Toolchain | 126 |
| 16 | QuickChick/QuickChick | Randomized Property-Based Testing Plugin for Coq | 118 |
| 17 | jwiegley/coq-haskell | A library for formalizing Haskell types and functions in Coq | 111 |
| 18 | jonleivent/mindless-coding | Mindless, verified (erasably) coding using dependent types | 104 |
| 19 | tchajed/coq-tricks | Tricks you wish the Coq manual told you | 101 |
| 20 | jwiegley/coq-pipes | 99 | |
| 21 | mit-plv/fiat-crypto | Cryptographic Primitive Code Generation by Fiat | 98 |
| 22 | coq-community/math-classes | A library of abstract interfaces for mathematical structures in Coq. | 94 |
| 23 | Ptival/PeaCoq | PeaCoq is a pretty Coq, isn't it? | 91 |
| 24 | uwplse/verdi-raft | An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework | 85 |
| 25 | amintimany/Categories | A formalization of category theory in the Coq proof assistant. | 78 |
| 26 | vellvm/vellvm | The Vellvm II coq development. | 77 |
| 27 | stepchowfun/proofs | A selection of formal developments in Coq. | 77 |
| 28 | discus-lang/iron | Coq formalizations of functional languages. | 77 |
| 29 | hazelgrove/hazel | Hazel, a live functional programming environment with typed holes | 77 |
| 30 | robbertkrebbers/ch2o | 73 | |
| 31 | mattam82/Coq-Equations | A plugin for Coq to add dependent pattern-matching. | 73 |
| 32 | TheoWinterhalter/formal-type-theory | Formalising Type Theory in a modular way for translations between type theories | 67 |
| 33 | DeepSpec/dsss17 | Lecture material for DeepSpec Summer School 2017 | 64 |
| 34 | coq-concurrency/pluto | A web server written in Coq. | 64 |
| 35 | clarus/falso | A proof of false. | 64 |
| 36 | coq-community/corn | Coq Repository at Nijmegen | 63 |
| 37 | TiarkRompf/scala-escape | A compiler plug-in to control object lifetimes in Scala | 58 |
| 38 | DistributedComponents/disel | Distributed Separation Logic: a framework for compositional verification of distributed protocols and their implementations. | 56 |
| 39 | sfja/sfja | SoftwareFoundations(Ja) | 55 |
| 40 | coq-ext-lib/coq-ext-lib | A library of Coq definitions, theorems, and tactics. | 54 |
| 41 | GeoCoq/GeoCoq | A formalization of geometry in Coq based on Tarski's axiom system | 53 |
| 42 | certichain/toychain | A minimalistic blockchain consensus implemented and verified in Coq | 52 |
| 43 | maximedenes/native-coq | Coq with native compilation, as well as machine integers and arrays ! | 50 |
| 44 | sec-bit/tokenlibs-with-proofs | 47 | |
| 45 | mit-plv/fiat | Mostly Automated Synthesis of Correct-by-Construction Programs | 47 |
| 46 | tcarstens/verlang | 45 | |
| 47 | pirapira/evmverif | An EVM code verification framework in Coq | 44 |
| 48 | sweirich/corespec | A Specification for Dependent Types in Haskell (Core) | 44 |
| 49 | cmeiklejohn/distributed-data-structures | Distributed Data Structures in Coq | 43 |
| 50 | clarus/coq-of-ocaml | Compile OCaml to Coq. | 41 |
| 51 | UniMath/TypeTheory | The mathematical study of type theories, in univalent foundations | 40 |
| 52 | smtcoq/smtcoq | Communication between Coq and SAT/SMT solvers | 39 |
| 53 | Karmaki/coq-dpdgraph | Build dependency graphs between COQ objects | 39 |
| 54 | pirapira/dry-analyzer | Dr. Y's Ethereum Contract Analyzer | 38 |
| 55 | ilyasergey/pnp | Lecture notes for a short course on proving/programming in Coq via SSReflect. | 38 |
| 56 | pi8027/lambda-calculus | A Formalization of Typed and Untyped λ-Calculi in SSReflect-Coq and Agda2 | 36 |
| 57 | TiarkRompf/minidot | Dependent Object Types (DOT), bottom up | 36 |
| 58 | samuelgruetter/dot-calculus | Formalization of the Dependent Object Types (DOT) calculus | 36 |
| 59 | wouter-swierstra/xmonad | xmonad in Coq | 34 |
| 60 | vellvm/vellvm-legacy | 34 | |
| 61 | coq-io/io | A library for effects in Coq. | 34 |
| 62 | plclub/metalib | The Penn Locally Nameless Metatheory Library | 33 |
| 63 | arthuraa/poleiro | A blog about Coq | 32 |
| 64 | querycert/qcert | Compilation and verification of data languages | 32 |
| 65 | jwiegley/bytestring-fiat | An implementation of the Haskell ByteString library using the Fiat system from MIT | 31 |
| 66 | mit-plv/bedrock2 | Towards a low-level systems programming language with a verified compiler | 31 |
| 67 | MichaelBurge/pornview | Porn browser formally-verified in Coq | 30 |
| 68 | accordproject/ergo | The Ergo Language for Smart Legal Contracts | 30 |
| 69 | aa755/ROSCoq | Robots powered by Constructive Reals | 30 |
| 70 | ejgallego/coq-serapi | Coq Protocol Playground with Se(xp)rialization of Internal Structures. | 30 |
| 71 | dbp/howtoproveacompiler | Writeup that goes along with this: | 29 |
| 72 | mit-plv/kami | A Platform for High-Level Parametric Hardware Specification and its Modular Verification | 28 |
| 73 | HIPERFIT/contracts | Symbolic financial contract EDSL | 28 |
| 74 | liufengyun/stoic | a capability-based system | 28 |
| 75 | pedagand/MPRI-2.4-DTP | MPRI-2.4 Dependently-typed Functional Programming | 27 |
| 76 | dschepler/coq-sequent-calculus | Coq formalizations of Sequent Calculus, Natural Deduction, etc. systems for propositional logic | 27 |
| 77 | plclub/cis670-16fa | Advanced Topics in Programming Languages, Penn CIS 670, Fall 2016 | 26 |
| 78 | sweirich/replib | Replib: generic programming & Unbound: generic treatment of binders | 26 |
| 79 | Template-Coq/template-coq | Reflection library for Coq | 25 |
| 80 | tezos/tezoscoq | working with coq and tezos | 24 |
| 81 | gtjennings1/UPDuino_v2_0 | UPDuino v2.0 - PCB Design Files, Designs, Documentation | 24 |
| 82 | vrahli/NuprlInCoq | Implementation of Nuprl's type theory in Coq | 23 |
| 83 | konne88/bagpipe | BGP Policy Verification | 22 |
| 84 | coq-contribs/coq-in-coq | A formalisation of the Calculus of Constructions | 22 |
| 85 | Javran/Thinking-dumps | This repo keeps track of my codes, answers and thinkings when exploring books. | 22 |
| 86 | adampetcher/fcf | Foundational Cryptography Framework for machine-checked proofs of cryptography. | 22 |
| 87 | amutake/actario | Verification Framework for Actor Systems on Coq | 22 |
| 88 | uds-psl/autosubst | Automation for de Bruijn syntax and substitution in Coq | 21 |
| 89 | andrejbauer/dedekind-reals | A formalization of the Dedekind reals in Coq | 21 |
| 90 | math-comp/analysis | Mathematical Components compliant Analysis Library | 21 |
| 91 | ropas/zooberry | A software framework for global sparse analyzers and their verified validators | 21 |
| 92 | bmsherman/topology | Formal topology (and some probability) in Coq | 20 |
| 93 | uwplse/CoqAST | Fun plugin to play with the Gallina AST. | 20 |
| 94 | Mtac2/Mtac2 | 20 | |
| 95 | coq-ext-lib/coq-compile | A compiler for Coq | 20 |
| 96 | gallais/parseque | Total Parser Combinators in Coq | 20 |
| 97 | CoqEAL/CoqEAL | CoqEAL -- The Coq Effective Algebra Library | 19 |
| 98 | DeepSpec/InteractionTrees | Formalization of the Interaction Tree Datatype in Coq | 19 |
| 99 | ANSSI-FR/FreeSpec | Modular Verification of Programs with Effects and Effect Handlers | 19 |
| 100 | ichistmeinname/free-proving | Resources for "One Monad to Prove Them All (Functional Pearl)" | 19 |
| 101 | ml4tp/gamepad | A Learning Environment for Theorem Proving | 19 |
| 102 | lastland/WebSpec | 18 | |
| 103 | lukaszcz/coqhammer | CoqHammer: An Automated Reasoning Hammer Tool for Coq | 18 |
| 104 | mit-frap/spring17 | Problem Sets for MIT 6.887 Formal Reasoning About Programs, Spring 2017 | 18 |
| 105 | ybertot/plugin_tutorials | A collection of small projects to illustrate how to write plugins for Coq | 18 |
| 106 | braibant/coq-tutorial-ml-tactics | A tutorial on how to write OCaml tactics for the Coq proof assistant | 18 |
| 107 | siddharthist/coq-big-o | A general yet easy-to-use formalization of Big O, Big Theta, and more based on seminormed vector spaces. | 18 |
| 108 | ppedrot/ltac2 | A standalone implementation of Ltac2 as a Coq plugin | 18 |
| 109 | heades/System-F-Coq | System F in coq. | 17 |
| 110 | coq-io/system | System effects for Coq. | 17 |
| 111 | jonleivent/mindless-coding-phase2 | Mindless, verified (erasably) coding using dependent types, phase 2 | 17 |
| 112 | pa-ba/calc-comp | Coq proofs for the paper "Calculating Correct Compilers" | 17 |
| 113 | gmalecha/mirror-core | A framework for extensible, reflective decision procedures. | 17 |
| 114 | unicoq/unicoq | An enhanced unification algorithm for Coq | 16 |
| 115 | jonsterling/coq-guarded-computational-type-theory | 16 | |
| 116 | haklabbeograd/software-foundations-coq-workshop | Materijal za radionicu Coq-a prema kursu "Software foundations" (CIS 500) Benjamina Piercea | 15 |
| 117 | inQWIRE/QWIRE | A quantum circuit language and formal verification tool | 15 |
| 118 | ekmett/homotopy | 15 | |
| 119 | coq-community/paramcoq | Coq plugin for parametricity | 15 |
| 120 | gmalecha/coq-interaction-trees | Co-inductive interaction trees provide a way to represent (potentially) non-terminating programs with I/O behavior. | 15 |
| 121 | jwiegley/linearscan | 15 | |
| 122 | reynir/Brainfuck | Brainfuck formalized in Coq | 15 |
| 123 | CertiKOS/coqrel | Binary logical relations library for the Coq proof assistant | 14 |
| 124 | gangtan/CPUmodels | GoNative project: formal machines models in Coq | 14 |
| 125 | nmvdw/Three-HITs | All higher inductive types can be obtained from three simple HITs. | 14 |
| 126 | dbp/howtoprovefullabstraction | Writeup that goes along with this: | 14 |
| 127 | finrod/System-T | Formalisation of Goedel's System T in Coq | 14 |
| 128 | cmeiklejohn/vvclocks | Verified vector clocks, with Coq! | 13 |
| 129 | mattam82/Constructors | Example Coq plugin | 13 |
| 130 | jasmin-lang/jasmin | Jasmin compiler | 13 |
| 131 | vlopezj/coq-course | Coq course at Chalmers CSE | 13 |
| 132 | mzp/msgpack-ocaml | MessagePack for OCaml/Coq | 13 |
| 133 | ynot-harvard/ynot | The Ynot Project source code. | 13 |
| 134 | rodrigogribeiro/unification | Formalisation of a type unification algorithm in Coq proof assistant. | 13 |
| 135 | micro-policies/micro-policies-coq | Coq formalization accompanying the paper: Micro-Policies: A Framework for Verified, Tag-Based Security Monitors | 13 |
| 136 | snu-sf/promising-coq | The Coq development of A Promising Semantics for Relaxed-Memory Concurrency | 13 |
| 137 | PrincetonUniversity/certicoq | 13 | |
| 138 | exercism/coq | Exercism exercises in Coq. | 12 |
| 139 | mit-plv/bbv | Bedrock Bit Vector Library | 12 |
| 140 | hivert/Coq-Combi | Algebraic Combinatorics in Coq | 12 |
| 141 | hypotext/linear-logic | An encoding of linear logic in Coq with minimal Sokoban and blocks world examples | 12 |
| 142 | Coq-Math-Problems/Problems | 12 | |
| 143 | robbertkrebbers/compcert | Fork of http://compcert.inria.fr/ | 12 |
| 144 | JasonGross/lob | Two attempts at formalizing Löb's Theorem, (one based on http://lesswrong.com/lw/t6/the_cartoon_guide_to_l%C3%B6bs_theorem/) | 12 |
| 145 | kushti/flp | Formalization of FLP Impossibility Theorem | 12 |
| 146 | GaloisInc/cryptol-semantics | Semantics for Cryptol | 12 |
| 147 | CategoricalData/HoTT-categories | A category theory library built on top of Homotopy Type Theory, based primarily on https://bitbucket.org/JasonGross/catdb, with some inspiration from https://github.com/benediktahrens/Foundations/tree/typesystems | 12 |
| 148 | uwplse/StructTact | Coq utility and tactic library. | 12 |
| 149 | 2xs/pipcore | 12 | |
| 150 | roglo/banach_tarski | Formal proof in Coq of Banach-Tarski paradox. | 12 |
| 151 | math-comp/finmap | Finset and finmap library | 12 |
| 152 | akr/codegen | Coq plugin for monomorphization and C code generation | 12 |
| 153 | mit-plv/bedrock | Coq library for verified low-level programming | 11 |
| 154 | maximedenes/coq-amd64 | 11 | |
| 155 | hephaestus-pl/coqfj | A mechanized proof of type safety for Featherweight Java using Coq | 11 |
| 156 | SkySkimmer/HoTTClasses | Like Math Classes but for HoTT | 11 |
| 157 | uwplse/PUMPKIN-PATCH | Proof Updater Mechanically Passing Knowledge Into New Proofs, Assisting The Coq Hacker | 11 |
| 158 | ilyasergey/scilla-coq | State-Transition Systems for Smart Contracts | 11 |
| 159 | shlevy/cat-fiat | An attempt to formalize unix cat in fiat | 11 |
| 160 | uwplse/cheerios | Formally verified Coq serialization library with support for extraction to OCaml | 11 |
| 161 | coq-contribs/semantics | A survey of semantics styles, from natural semantics through structural operational, axiomatic, and denotational semantics, to abstract interpretation. | 11 |
| 162 | mit-frap/spring18 | Problem Sets for MIT 6.822 Formal Reasoning About Programs, Spring 2018 | 10 |
| 163 | SimonBoulier/TypingFlags | A Coq plugin to disable positivity check, guard check and termination check | 10 |
| 164 | bacam/coqjvm | Coq executable semantics and resource verifier | 10 |
| 165 | braibant/Synthesis | 10 | |
| 166 | mzp/coq-ruby | 10 | |
| 167 | MarisaKirisame/Coq_code | 10 | |
| 168 | mit-pdos/6.826-2017-labs | 10 | |
| 169 | julbinb/concept-params | Coq formalization of "concept parameters" for "generic" programming in STLC | 10 |
| 170 | JasonGross/coq-tactics | Collection of tactics I've found useful in Coq | 10 |
| 171 | ekmett/comonad-transformers | Haskell 98 comonad transformers - as of 4.0 these have merged into the comonad package. | 10 |
| 172 | hablapps/LensStateIsYourFather | Lens, State is your father... and I can prove It! | 9 |
| 173 | CertiKOS/compcert.old | CompCertX features to be merged into CompCert | 9 |
| 174 | nbenton/coqdomains | Domain theory and denotational semantics in Coq | 9 |
| 175 | AdaCore/why3 | SPARK 2014 repository for the Why3 verification platform. | 9 |
| 176 | bitemyapp/ledgertheory | 9 | |
| 177 | akr/coq-html-escape | 9 | |
| 178 | jwiegley/coq-lattice | A reflection-based proof tactic for lattices in Coq | 9 |
| 179 | dschepler/coq-topology | Topology library for Coq | 9 |
| 180 | brunofx86/LL | Formalization of Linear Logic | 9 |
| 181 | uwplse/oeuf | gallina frontend for CompCert | 9 |
| 182 | amaurremi/dot-calculus | Adding extensions to DOT calculus | 9 |
| 183 | rfindler/395-2013 | 9 | |
| 184 | acowley/LinearLogic | A simple development of linear logic in Coq. | 9 |
| 185 | gmalecha/coq-ltac-iter | Access hint databases from tactics. | 9 |
| 186 | csgordon/coq-fsharp | Libraries and tools for extracting Coq code to F# | 9 |
| 187 | sunblaze-ucb/coq-smart-contract | 9 | |
| 188 | kalfazed/Coq---Programming-Language | Haskell函数式编程的代码实例以及教程 | 8 |
| 189 | daniellustig/pipecheck | 8 | |
| 190 | coq-io/hello-world | A Hello World program in Coq. | 8 |
| 191 | konne88/SpaceSearch | 8 | |
| 192 | mzp/coq-for-ipad | 8 | |
| 193 | tchajed/coq-io | Modeling I/O in Coq using free monads | 8 |
| 194 | fpottier/minirust | A tentative formalisation of mini-Rust. | 8 |
| 195 | mattam82/Forcing | Forcing layer on top of Coq | 8 |
| 196 | foreverbell/verified | Coq formalizations and proofs of (data) structures and algorithms. | 8 |
| 197 | hemmi/coq2scala | 8 | |
| 198 | jmadiot/coq100 | Statement of theorems proven in Coq | 8 |
| 199 | peterlefanulumsdaine/hott-limits | A formalization of (homotopy) limits in Homotopy Type Theory | 8 |
| 200 | bobatkey/system-f-parametricity-model | A Model of Relationally Parametric System F in Coq | 8 |
| 201 | damien-pous/relation-algebra | Relation algebra library for Coq | 8 |
| 202 | tmiya/coq | My Coq codes | 8 |
| 203 | mmcco/Verified-BPF | Initial tinkering with a BPF metalanguage and implementation formally verified in Coq. | 8 |
| 204 | jdoughertyii/hott-species | Combinatorial species in HoTT | 8 |
| 205 | xavierleroy/coq2html | An HTML documentation generator for Coq source files | 8 |
| 206 | kendroe/CoqPIE | CoqPIE (an IDE for the Coq theorem prover + PEDANTIC) | 7 |
| 207 | tangentforks/FourColorTheorem | Gonthier's formal proof of the 4-color theorem, in Coq. | 7 |
| 208 | wangpengmit/6887psets | Problem Sets for MIT 6.887 Formal Reasoning About Programs | 7 |
| 209 | coq-contribs/topology | General Topology | 7 |
| 210 | csvoss/coqingbird | To Mock a Mockingbird, formalized in Coq | 7 |
| 211 | suharahiromichi/coq | Coq Code | 7 |
| 212 | frenetic-lang/netkat | Starting a Coq NetKAT | 7 |
| 213 | pa-ba/McCarthy-Painter | Coq proof for the paper "Compiling a Fifty Year Journey" | 7 |
| 214 | mmaleki/LogicalDifferentiation | Differentiation in logical form by Stone duality. | 7 |
| 215 | pi8027/formalized-postscript | PostScript programming in the Coq proof assistant | 7 |
| 216 | FTRobbin/Ironwood | A Correct-by-Construction Blockchain Protocol Implementation | 7 |
| 217 | cpdt-japanese/cpdt-japanese | Certified Programming with Dependent Types (Japanese Translation) | 7 |
| 218 | tymmym/software-foundations | Solutions to the exercises from the 'Software Foundations' book by Benjamin Pierce et al. | 7 |
| 219 | QuickChick/IFC | Information Flow Control (IFC) case study for the QuickChick testing plugin for Coq. Includes verification of testing and some other Coq proofs. | 7 |
| 220 | fpottier/dblib | 7 | |
| 221 | tlively/BrainCoqulus | A formally verified compiler of untyped lambda calculus to brainfuck | 7 |
| 222 | DistributedComponents/verdi-chord | An implementation of the Chord lookup protocol verified in Coq using the Verdi framework | 7 |
| 223 | EasyCrypt/certicrypt | CertiCrypt Coq Framework | 7 |
| 224 | amutake/coq-extensible-effects | Extensible Effects in Coq | 7 |
| 225 | QinxiangCao/UnifySL | 7 | |
| 226 | tchajed/coq-tactical | Library of Coq proof automation | 7 |
| 227 | pedagand/coq-label | Labels for Coq | 7 |
| 228 | tchajed/goedel-t | Formalization of termination of Gödel's System T | 7 |
| 229 | pleiad/Refinements | Experiments in formalizing refinement type systems in Coq | 7 |
| 230 | mroman42/math | 7 | |
| 231 | kit-ty-kate/why3 | An unofficial mirror of Why3 (http://why3.lri.fr/) | 7 |
| 232 | dboulytchev/miniKanren-coq | A certified semantics for relational programming workout. | 7 |
| 233 | mit-plv/riscv-coq | RISC-V Specification in Coq | 7 |
| 234 | engboris/term-rewriting | Personal study of abstract term rewriting with Coq | 7 |
| 235 | arthuraa/cufp-2015-tutorial | An introductory tutorial for the Coq proof assistant. | 7 |
| 236 | imdea-software/fcsl-pcm | Partial Commutative Monoids | 7 |
| 237 | SkySkimmer/HoTT-algebra | Coq formalisation of algebra in Homotopy Type Theory | 6 |
| 238 | antalsz/urn-random | A Haskell package for updatable discrete distributions | 6 |
| 239 | jwiegley/set-theory | 6 | |
| 240 | Barry-Jay/SF | Coq implementation of SF-calculus and the tranlsation to it of lift lambda-calculus | 6 |
| 241 | Operational-Transformation/ot.v | Formalisation of Operational Transformation in Coq | 6 |
| 242 | coq-contribs/ieee754 | A formalisation of the IEEE754 norm on floating-point arithmetic | 6 |
| 243 | math-comp/multinomials | Multinomials for Ssreflect | 6 |
| 244 | readablesystems/cs260r-17 | Main repository for Harvard CS260r 2017. | 6 |
| 245 | coq-contribs/atbr | A tactic for deciding Kleene algebras | 6 |
| 246 | aa755/paramcoq-iff | 6 | |
| 247 | ulysses4ever/certif-sw-2014 | 6 | |
| 248 | ezyang/HoTT-coqex | Coq solutions to exercises in HoTT book | 6 |
| 249 | clarus/cybele | A Coq plugin for simpler proofs by reflection or OCaml certificates. | 6 |
| 250 | gmalecha/coq-smt-check | Invoke SMT solvers from Coq to check obligations | 6 |
| 251 | mir-ikbch/compl_coq | 6 | |
| 252 | coq-contribs/automata | Beginning of formal language theory | 6 |
| 253 | MathiasVP/ni-formal-gc | Coq formalization of timing-sensitive noninterference for a garbage collected language with heap and runtime pc level. | 6 |
| 254 | mmcco/verified-parser-example | A minimal example of a formally verified parser using ocamllex and Menhir's Coq backend. | 6 |
| 255 | coq-contribs/pi-calc | Pi-calculus in Coq | 6 |
| 256 | PrincetonUniversity/compcomp | Compositional CompCert | 6 |
| 257 | fblanqui/color | Coq library on rewriting theory and termination | 6 |
| 258 | gmalecha/mirror-shard | Reflective verification procedures for separation logic programs in Coq | 6 |
| 259 | DistributedComponents/InfSeqExt | A Coq library for reasoning (co)inductively on infinite sequences using LTL-like modal operators | 6 |
| 260 | relrod/ct | My attempt to better understand both Coq and Category Theory by formalizing the latter in the former. | 6 |
| 261 | kristinas/hinitiality | 6 | |
| 262 | ProgVal/LambdaCert | LambdaJS interpreter. | 6 |
| 263 | thoughtpolice/coq-skeleton | A simple skeleton for Coq projects | 6 |
| 264 | vladoovtcharov/Software-Foundations-Solutions | Working on some solutions to http://www.cis.upenn.edu/~bcpierce/sf/ | 6 |
| 265 | sifive/Kami | 6 | |
| 266 | vrahli/Velisarios | 6 | |
| 267 | coq-contribs/relation-algebra | Relation Algebra and KAT | 5 |
| 268 | arthuraa/memory-safe-language | A formalization of properties of a simple imperative, memory-safe language. | 5 |
| 269 | aa755/CFGV | A generic library for reasoning about languages with binders | 5 |
| 270 | snu-sf/crellvm | Crellvm: Verified Credible Compilation for LLVM | 5 |
| 271 | FlorianSteinberg/coqrep | 5 | |
| 272 | LS-Lab/Coq-dL | A formally verified implementation of differential dynamic logic in Coq | 5 |
| 273 | mit-pdos/cspec | Verifying concurrent code with layers and movers | 5 |
| 274 | coq/bignums | Coq library of arbitrary large numbers. Provides BigN, BigZ, BigQ that used to be part of Coq standard library | 5 |
| 275 | tchajed/regex-derivative | Regex derivatives in Coq | 5 |
| 276 | SamB/coq | git-svn mirror of Coq + branches -- see http://github.com/SamB/coq/wikis | 5 |
| 277 | uwplse/crimp | Certified Relational to Imperative | 5 |
| 278 | sftypes/software-foundations | Coq proofs of exercises in Pierce's book | 5 |
| 279 | jtcriswell/Pudding | KCoFI Pudding: The formal proofs for the KCoFI system | 5 |
| 280 | nhojem/Coq-Polyhedra | Formalizing convex polyhedra in Coq | 5 |
| 281 | coq-contribs/cats-in-zfc | Category theory in ZFC | 5 |
| 282 | izgzhen/iris-c-coq | Control-flow based language verification framework | 5 |
| 283 | coq-contribs/regexp | Regular Expression | 5 |
| 284 | amintimany/CTDT | Category-theoretic domain theory. | 5 |
| 285 | amintimany/OPLSS | 5 | |
| 286 | y-taka-23/concepts-of-proglangs | 五十嵐淳『プログラミング言語の基礎概念』の Coq による実装 | 5 |
| 287 | mgrabovsky/fm-notes | Unassorted scribbles on formal methods, type theory, category theory, and so on, and so on | 5 |
| 288 | atlanmod/CoqTL | 5 | |
| 289 | tm507211/CoqPerceptron | Verified Coq Implementation of the Perceptron Algorithm | 5 |
| 290 | gmalecha/bedrock-mirror-shard | Port of Bedrock to use MirrorShard library for computational reflection | 5 |
| 291 | wouter-swierstra/Bird | Formalization of Richard Bird's Pearls of Functional Algorithm Design | 5 |
| 292 | serras/sf-exercises | 5 | |
| 293 | ppedrot/coq-forcing | Tentative implementation of call-by-name forcing in Coq | 5 |
| 294 | JasonGross/slow-coq-examples | Examples of Coq being really slow | 5 |
| 295 | mit-pdos/deepspec-pocs | 5 | |
| 296 | chdoc/coq-reglang | Regular Language Representations in the Constructive Type Theory of Coq | 5 |
| 297 | jaredly/coqdocs | The docs I wish I had while learning Coq | 5 |
| 298 | wjzz/Agda-small-developments-and-examples | A collection of mostly unrelated Agda programs which I found interesting in some way. | 5 |
| 299 | coqtail/coqtail | 5 | |
| 300 | roglo/cauchy_schwarz | Formal proof in Coq of Cauchy Schwarz Inequality | 5 |
| 301 | DistributedComponents/verdi-lockserv | An implementation of a simple asynchronous message-passing lock server, verified in Coq using the Verdi framework | 5 |
| 302 | coq-contribs/pts | A formalisation of Pure Type Systems | 5 |
| 303 | jonsterling/coq-meaning-explanation | 5 | |
| 304 | FFaissole/Valuations | Synthetic Topology in Homotopy Type Theory for probabilstic programming | 5 |
| 305 | fmota/coq-space | Constructive General Topology in Coq (WIP) | 5 |
| 306 | Kiarahmani/Quelea_Coq_Imp | An Implementation of Quelea (http://gowthamk.github.io/docs/quelea.pdf) in Coq | 5 |
| 307 | AshleyYakeley/maths | Just trying to learn Coq. | 5 |
| 308 | CoqHott/coq-effects | A program translation implementing self-algebraic effects in Coq. | 5 |
| 309 | digamma-ai/asn1fpcoq | Coq formalization of ASN.1 floating point | 5 |
| 310 | tabareau/Cocasse | A library for Gradual Certified Programming in Coq | 5 |
| 311 | braibant/exploit-plugin | An OCaml version of the LTac "exploit" tactic, used as a tutorial for writing Coq plugins | 5 |
| 312 | gclaramunt/CoqWorkshop | 5 | |
| 313 | ezrakilty/hillel-challenge | An attempt to solve the problems of Hillelogram at https://twitter.com/Hillelogram/status/987432181889994759 | 5 |
| 314 | vafeiadis/hahn | Hahn: A Coq library | 5 |
| 315 | yugithub/OFDM-baseband | Verilog实现OFDM基带 | 5 |
| 316 | jan-christiansen/Language-based-Security | Course Language-based Security at Flensburg University of Applied Sciences | 5 |
| 317 | 5HT/co | CoInductive Shell in Coq | 5 |
| 318 | ankitku/TAL0 | Based on paper by Greg Morrisett , TAL-0 is the design of a RISC-style typed assembly language which focuses on control-flow safety. | 5 |
| 319 | jihgfee/coq-system_f | A simple encoding of the System F language in Coq | 5 |
| 320 | robdockins/domains | A formal development of constructive domain theory in Coq | 4 |
| 321 | thery/PolTac | Tactic for polynomial manipulations | 4 |
| 322 | clarus/phd-experiments | Experiments I am doing for my PhD | 4 |
| 323 | coq-community/aac-tactics | This Coq plugin provides tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators. | 4 |
| 324 | stonebuddha/eopl | Essentials of Programming Languages, with OCaml implementations & Coq proofs | 4 |
| 325 | gmalecha/coq-plugin-utils | Useful utility functions for writing Coq plugins | 4 |
| 326 | coq-concurrency/proxy | A proxy to interface concurrent Coq programs with the operating system. | 4 |
| 327 | herbelin/coq-hh | Hugo Herbelin's public Coq branches | 4 |
| 328 | benediktahrens/monads | Coq code accompanying several articles on semantics of functional programming languages | 4 |
| 329 | kolemannix/oplss2015 | Notes and Materials from OPLSS 2015 | 4 |
| 330 | jdoughertyii/hott-exercises | Exercises from The HoTT Book by hand and by Coq | 4 |
| 331 | mzp/coq-ide-for-ios | 4 | |
| 332 | CoqHott/Program-translations-CC-omega | 4 | |
| 333 | mzp/coq-js | 4 | |
| 334 | aspiwack/finset | A Coq library for extensional finite sets and comprehension | 4 |
| 335 | rf0444/coq | Coq 練習など | 4 |
| 336 | LoukaSoret/Stage2017_COQ | La logique du premier ordre prouvée avec Coq | 4 |
| 337 | fetburner/Coq2SML | 4 | |
| 338 | JetBrains/ot-coq | ot-coq | 4 |
| 339 | secure-compilation/exploring-robust-property-preservation | Supplementary material for Exploring Robust Property Preservation for Secure Compilation | 4 |
| 340 | GavinMendelGleason/code | All of the random projects, test files, helloworlds, proofs etc. | 4 |
| 341 | imdea-software/htt | Hoare Type Theory | 4 |
| 342 | CategoricalData/catdb | 4 | |
| 343 | clarus/coq-cunit | Convenience functions for unit testing in Coq. | 4 |
| 344 | google/coq-bpf | Coq BPF interpreter | 4 |
| 345 | yoshihiro503/coqQuickCheck | QuickCheck for Coq | 4 |
| 346 | vsiles/regexp-Brzozowski | Coq files for the formalization of "A Decision Procedure for Regular Expression Equivalence in Type Theory" by Thierry Coquand and myself | 4 |
| 347 | hephaestus-pl/hffj | An implementation of Feature Featherweight Java (FFJ) using Hephaestus. | 4 |
| 348 | secworks/cmac | Implementation of the CMAC keyed hash function using AES as block cipher. | 4 |
| 349 | coq-contribs/lin-alg | Linear Algebra | 4 |
| 350 | daniellustig/coatcheck | COATCheck | 4 |
| 351 | stepchowfun/coq-intro | An introduction to proving theorems and certifying programs with Coq. | 4 |
| 352 | bollu/polyir | A semantics for the types of loops that can be modelled by polyhedral compilation techniques, developed in Coq. | 4 |
| 353 | CUTE-Lang/CUTE-spec | Specification Documents for CUTE Lang | 4 |
| 354 | dragonwasrobot/simpl-lang | A simple language created in Coq, batteries and correctness proofs included. | 4 |
| 355 | GU-CLASP/FraCoq | Coq semantics for the GF FraCas suite | 4 |
| 356 | BenjaminCHEN2016/FunctionalProgramming | Code for 2018 Functional Programming | 4 |
| 357 | raaz-crypto/verse-coq | VERified asSembler for cryptographic primitives | 4 |
| 358 | amutake/a-pi | Formalization of Aπ-calculus in Coq | 4 |
| 359 | martijnvermaat/infinitary-rewriting-coq | Infinitary Rewriting in Coq | 4 |
| 360 | PrincetonUniversity/DeepSpecDB | 4 | |
| 361 | affeldt-aist/monae | 4 | |
| 362 | dandougherty/mqpCoq2018 | 4 | |
| 363 | dschepler/coq-zorns-lemma | Naive set theory library for Coq | 4 |
| 364 | Eelis/hybrid | Certified implementation of abstraction-based hybrid system safety prover. | 4 |
| 365 | reservoirlabs/vsarbp | Verified SAR-BP: a verified C implementation of Synthetic Aperture Radar backprojection with certified absolute error bound | 4 |
| 366 | xnning/Consistent-Subtyping-for-All | Supplementary materials for paper Consistent Subtyping for All published in ESOP 2018 and its follow-up journal submission | 4 |
| 367 | samuelgruetter/riscv-coq | RISC-V Specification in Coq | 4 |
| 368 | cogumbreiro/brenner-coq | Brenner is a calculus for reasoning about task parallelism and barrier synchronization. This calculus distils the semantics of phasers and unifies the synchronisation patterns of various abstractions. | 4 |
| 369 | wrengr/coq-wrengr-util | Tactics, utility lemmas, and relation combinators for Coq | 4 |
| 370 | affeldt-aist/infotheo | 4 | |
| 371 | mattam82/opetopic-coq | Port of Eric Finster's opetopic types to Coq. | 4 |
| 372 | aspiwack/cosa | A thing about Coq-verified Shape Analysis | 4 |
| 373 | coq-contribs/ltl | Linear Temporal Logic | 4 |
| 374 | QuentinFiard/CoqCertifiedCompiler | A compiler for a very simple language, certified in Coq | 4 |
| 375 | gmalecha/coq-markov | Exploring probabilistic programming in Coq | 4 |
| 376 | gmalecha/coq-lens | Lenses in Coq | 4 |
| 377 | nbenton/x86proved | 4 | |
| 378 | airobo/Project-Euler-in-Coq | 4 | |
| 379 | wilcoxjay/tactics | some Coq tactics I've found useful | 4 |
| 380 | Zimmi48/transfer | Automatic transfer of theorems along isomorphisms in Coq | 4 |
| 381 | haslab/CircGen | 4 | |
| 382 | hablapps/LensAlgebra | Towards Optic-Based Algebraic Theories: the Case of Lenses | 4 |
| 383 | channgo2203/fevm | Formalization of EVM in Coq | 4 |
| 384 | cjerdonek/formal-rcv | Formal specifications of ranked choice voting and related developments | 4 |
| 385 | arthuraa/extructures | Finite sets and maps for Coq with extensional equality | 3 |
| 386 | cogumbreiro/aniceto-coq | Aniceto is a library that helps Coq development. It includes a libray of properties on graph theory. | 3 |
| 387 | jonsterling/Coq-Up | A tarpit in Coq | 3 |
| 388 | vmurali/SeqConsistency | 3 | |
| 389 | Zeimer/CoqBookPL | Źródła mojej książki o Coqu, logice konstruktywnej, programowaniu funkcyjnym i innych takich. | 3 |
| 390 | hablapps/koky | Typeclasses, datatypes and theorems for functional programming in Coq. | 3 |
| 391 | brownplt/ProgressiveTypes | 3 | |
| 392 | secure-compilation/when-good-components-go-bad | Coq formalization for "When Good Components Go Bad" paper | 3 |
| 393 | coq-contribs/zfc | An encoding of Zermelo-Fraenkel Set Theory in Coq | 3 |
| 394 | plietar/formal-pony | 3 | |
| 395 | CoqHott/DICoq | Dependent Interoperability for Coq | 3 |
| 396 | yoshihiro503/coqio | Coq IO | 3 |
| 397 | philipjf/AWG-AVOCS-2016 | An Arbitrary Waveform Generator | 3 |
| 398 | CoqHott/coq-forcing | A plugin for Coq that implements the call-by-name forcing translation | 3 |
| 399 | armoredsoftware/session | Dependent Session Types | 3 |
| 400 | Matafou/ill_narratives | A development of a subset of intuitionistic linear logic, suitable for representing narratives. | 3 |
| 401 | KyushuUniversityMathematics/TPP2014 | Theorem proving and provers for reliable theory and implementations | 3 |
| 402 | coq-contribs/group-theory | Elements of Group Theory | 3 |
| 403 | jalpuim/disjoint-intersection-types | Supplementary material for the paper Disjoint Intersection Types, namely Coq proofs and implementation. | 3 |
| 404 | mboes/coqine | An encoding of the Calculus of Inductive Constructions (as implemented in Coq) in Dedukti. | 3 |
| 405 | rnrand/VPHL | Coq development for VPHL: A Verified Partial-Correctness Logic for Probabilistic Programs, MFPS 2015 | 3 |
| 406 | wenkokke/EnumeratingTheRationals | a formalisation of the functional pearl "Enumerating the Rationals" by Gibbons, Lester and Bird in Coq | 3 |
| 407 | coq-contribs/gc | Formal Verification of an Incremental Garbage Collector | 3 |
| 408 | clarus/coq-list-string | Strings implemented as lists. | 3 |
| 409 | MurataKosuke/human-readable_proofs | Coq tactic library for human-readable proofs based on formula rewriting | 3 |
| 410 | gstew5/cage | 3 | |
| 411 | uwplse/peek | Peek: a verified peephole optimizer for CompCert | 3 |
| 412 | jesper-bengtson/ChargeCore | 3 | |
| 413 | coq-contribs/graph-basics | a Coq toolkit for graph theory | 3 |
| 414 | akr/monadification | Coq plugin for monadification | 3 |
| 415 | JasonGross/parsing-parses | A dependently typed parser that parses parse trees to prove itself sound and complete | 3 |
| 416 | kit-ty-kate/coq-playground | Playing with Coq… | 3 |
| 417 | fpottier/loop | 3 | |
| 418 | sigurdschneider/smpl | A Coq plugin providing an extensible tactic similar to first. | 3 |
| 419 | CoqHott/exceptional-tt | A Coq plugin that implements exceptions in Coq | 3 |
| 420 | nunchaku-inria/nunchaku-coq | [not-working] Coq plugin for using Nunchaku from Coq | 3 |
| 421 | pilki/coq2tex | Produce LaTeX code from Coq | 3 |
| 422 | picnic/RelationExtraction | Inductive relations extraction plugin for Coq | 3 |
| 423 | pa-ba/cps-defun | Coq proofs for the paper "Cutting out Continuations" | 3 |
| 424 | mit-frap/spring16 | Problem Sets for MIT 6.887 Formal Reasoning About Programs, Spring 2016 | 3 |
| 425 | MichaelBurge/goodsteins-theorem | A formal proof of Goodstein's theorem | 3 |
| 426 | fetburner/TypeInfer | A Formal Verification of Algorithm W | 3 |
| 427 | pi8027/efficient-finfun | 3 | |
| 428 | jwiegley/refine-freer | Experiments with an extensible refinement framework | 3 |
| 429 | meta-logic/coq-ll | Formalization of Linear Logic in Coq | 3 |
| 430 | plietar/pony-proofs | 3 | |
| 431 | coq-contribs/coinductive-reals | Real numbers as coinductive ternary streams | 3 |
| 432 | Zeimer/CoqCat | Formalization of Category Theory in Coq. | 3 |
| 433 | coq-contribs/algebra | Basics notions of algebra | 3 |
| 434 | mit-plv/stencils | A Coq library for verifying dependencies of stencil implementations | 3 |
| 435 | fsmith1024/scales | Formalization in Coq of recreational puzzles involving scales. | 3 |
| 436 | Ekdohibs/coq-proofs | Various proofs in Coq. As of now, only contains the proof of the theorem of quadratic reciprocity. | 3 |
| 437 | ConsensusResearch/MultiBranch | MultiBranch Forging Simulation Tool | 3 |
| 438 | mattam82/Coq-unif | Formalization of unification in Coq | 3 |
| 439 | coq-contribs/coalgebras | Coalgebras, bisimulation and lambda-coiteration | 3 |
| 440 | dricketts/quadcopter | 3 | |
| 441 | erikhpalmgren/LCC_setoids_in_Coq | Coq proofs of categorical properties of setoids: local cartesian closedure and existence of coequalizers | 3 |
| 442 | qnighy/IPC-Coq | Intuitionistic Propositional Calculus | 3 |
| 443 | JasonGross/ct4s | Exercises for Category Theory For Scientists (18.S996, Spring 2013, http://math.mit.edu/~dspivak/teaching/sp13/) | 3 |
| 444 | knuton/la-girafe-sportive | Coq-verified statements about lambda calculi. | 3 |
| 445 | rafaelcgs10/Anti-Unification-Algorithm | This is the Coq formalization of an anti-unification algorithm for my master thesis. | 3 |
| 446 | coq-contribs/finger-tree | Dependent Finger Trees | 3 |
| 447 | CuMathInfo/Topology | Formalization of topology | 3 |
| 448 | jwiegley/zomega | A computational reflection based solver for expressions involving Z (but tunable) | 3 |
| 449 | dbp/literatecoq | 3 | |
| 450 | wrengr/coq-tutorial | 3 | |
| 451 | coq-contribs/containers | Containers: a typeclass-based library of finite sets/maps | 3 |
| 452 | sighingnow/amazing-coq | WHAT I have done on the road to Coq language and certified programming. | 3 |
| 453 | secworks/siphash | Hardware implementation of the SipHash keyed hash function | 3 |
| 454 | math-comp/odd-order | The formal proof of the Odd Order Theorem | 3 |
| 455 | OKU1987/FJ_whoas | 3 | |
| 456 | runarorama/sannanir | 3 | |
| 457 | khibino/sfja-code | Codes for 'Software Foundations' | 3 |
| 458 | bmsherman/finite | Facts about isomorphisms and finite types in Coq | 3 |
| 459 | coqoon/Software-Foundations | 3 | |
| 460 | yurug/coqepit | Your research in Coq | 3 |
| 461 | clarus/coq-atm | A verified ATM program in Coq. | 3 |
| 462 | hubbards/stlc-coq | Simply typed lambda calculus in Coq | 3 |
| 463 | sun12jun/ARM9_THUMB_RTL | arm9 thumb processor | 3 |
| 464 | upscent/memo | 3 | |
| 465 | amosr/coq | 3 | |
| 466 | sutajiokousagi/kovan-test-fpga | A version of the FPGA that shows a test pattern on HDMI | 3 |
| 467 | sigurdschneider/lvc | LVC verified compiler | 3 |
| 468 | coq-io/experiments | Experiments with Coq effects. | 3 |
| 469 | pi8027/sandpit | 3 | |
| 470 | input-output-hk/qeditas-ledgertheory | Coq development of a theory of lightweight cryptographic ledgers | 3 |
| 471 | liyishuai/cps | Conversion from System T to continuation-passing style (CPS) | 3 |
| 472 | roglo/puiseuxth | Formal proof in Coq of Puiseux's Theorem. | 3 |
| 473 | pqwy/colorless-green-ideas | No description, website, or topics provided. | 3 |
| 474 | jesper-bengtson/Java | A model of Java in Coq based on the Charge! framework. | 3 |
| 475 | Paradoxika/ModalLogic | Automated Reasoning for Modal Logics | 3 |
| 476 | jbapple/priority-queues | Automatically exported from code.google.com/p/priority-queues | 3 |
| 477 | coq-contribs/lesniewski-mereology | LesniewskiMereology is a Coq library created by R. Dapoigny and P. Barlatier whose purpose is to implement the alternative to Set Theory of Stanislaw Lesniewski. It is part of an on-going project using the Coq language and called KDTL (Knowledge-based Dependently Typed Language) to build an alternative to Description Logics. The developed theory is close to the analysis of Denis Mieville (1984) in his book "Un developpement des systemes logiques de Stanislaw Lesniewski". It is a theoretical construct which relies on three dependent levels, logic (a.k.a. Protothetic), the Lesniewski Ontologie (LO) and mereology. Each level incorporates a minimal collection of axioms, protothetic and ontologic definitions and a set of theorems together with their intuitionist proofs. | 2 |
| 478 | andorp/cpdt | Certified Programming with Dependent Types - examples, learning material. | 2 |
| 479 | affeldt/ssrcoq-kyoto2015 | 2 | |
| 480 | secure-compilation/beyond-good-and-evil | Auxiliary materials for "Beyond Good and Evil" paper | 2 |
| 481 | VERIMAG-Polyhedra/VplTactic | A Coq Tactic for Arithmetic (based on VPL) | 2 |
| 482 | brownplt/lambdajs-coq | 2 | |
| 483 | coq-contribs/quicksort-complexity | Proofs of Quicksort's worst- and average-case complexity | 2 |
| 484 | dragonwasrobot/formal-moessner | A formal study of Moessner's sieve | 2 |
| 485 | FreeAndFair/OpenRLA | Free & Fair's open source RLA support software. | 2 |
| 486 | LukeXuan/formal-logic | 2 | |
| 487 | mattam82/Coq-misc | Misc hacks on Coq | 2 |
| 488 | amahboubi/lia4mathcomp | Preprocessing goals featuring mathcomp style operations before applying the lia tactic. | 2 |
| 489 | reservoirlabs/vcfloat | VCFloat: A Unified Coq Framework for Verifying C Programs with Floating-Point Computations | 2 |
| 490 | Warbo/powerplay | Mirror of http://chriswarbo.net/git/powerplay | 2 |
| 491 | asherrecv/coq-shortest-path | 2 | |
| 492 | JasonGross/adt-synthesis | Repo for ADT Synthesis work, to eventually be integrated into github | 2 |
| 493 | konne88/konne88.github.io | Homepage | 2 |
| 494 | csgordon/guarded-recursion | Playing with guarded recursion in Coq and Agda | 2 |
| 495 | ppashakhanloo/verilog-adders | Implementation of different types of adder circuits | 2 |
| 496 | voellinger/verified-certifying-distributed-algorithms | A collection of verified certifying distributed algorithms. | 2 |
| 497 | waylang/infrastructure | Project Lifecycle and Tooling | 2 |
| 498 | coq-contribs/rsa | Correctness of RSA algorithm | 2 |
| 499 | coq-contribs/lambek | A Coq Toolkit for Lambek Calculus | 2 |
| 500 | themattchan/software-foundations | Learning formal verification. | 2 |
| 501 | FreeAndFair/formal-rcv | Some formalized developments of ranked-choice and instant-runoff voting schemes in Coq | 2 |
| 502 | kik/sandbox | sandbox | 2 |
| 503 | coq-contribs/fundamental-arithmetics | Fundamental theorems of arithmetic | 2 |
| 504 | coq-contribs/markov | Markov's inequality | 2 |
| 505 | izgzhen/iris-coq | a non-maintained mirror repo of https://gitlab.mpi-sws.org/FP/iris-coq/ | 2 |
| 506 | STFleming/StitchUp | StitchUp is a plugin to the LegUp High Level Synthesis tool that enables the generation of fault tolerant FPGA circuits. | 2 |
| 507 | mbrcknl/ylj15-coq-pattern-match | Code from a talk given at YOW! Lambda Jam 2015 | 2 |
| 508 | Barry-Jay/lambdaSF | implementation of lambda-SF-calculus plus some basic theorems | 2 |
| 509 | zhiyuanshi/intersection | 2 | |
| 510 | KevinQuirin/sheafification | Sheafification functor in type theory | 2 |
| 511 | pirapira/token_why3 | A Why3 modelling of a token contract | 2 |
| 512 | KyushuUniversityMathematics/RelationalCalculus | 2 | |
| 513 | coq-contribs/sudoku | A certified Sudoku solver | 2 |
| 514 | lkilcher/pyTurbSim | pyTurbSim is a turbulence simulation tool for HydroKinetic (tidal, river and ocean-current) turbine device design tools (e.g. NWTC's FAST). It is also an effective development platform for new TurbSim spectral models. | 2 |
| 515 | pi8027/vass | 2 | |
| 516 | kelloggm/kodellama2 | Interpreter for the Kodellama language that we have created. Project for CS4240 Fall 2014 at UVA. | 2 |
| 517 | wangpengmit/ssmatrix-theory | Coq formalization of matrix differentiation | 2 |
| 518 | hivert/Coq-HookLength | 2 | |
| 519 | txyyss/Formal-Mathematics | Mathematics in Coq | 2 |
| 520 | braibant/hash-consing-coq | 2 | |
| 521 | duckki/bedrock-examples | 2 | |
| 522 | jwiegley/fiat-rel | An exploration into using type classes with heterogenous relations to automate type refinement in Fiat | 2 |
| 523 | input-output-hk/qeditas-cryptohash | Coq code demonstrating a method for representing and reasoning about idealized cryptographic hashing functions | 2 |
| 524 | fetburner/Misc | Misc programs | 2 |
| 525 | coq-io/checker | Automatic checker for lock-free concurrent programs in Coq. | 2 |
| 526 | lpw25/row-subtyping | Row subtyping | 2 |
| 527 | g-hyoga/software-foundation | http://proofcafe.org/sf/ これをやる | 2 |
| 528 | mvmramos/chomsky | 2 | |
| 529 | jledent/vset | The cumulative hierarchy V | 2 |
| 530 | mathink/mpl | Monads with Predicate Liftings in Coq | 2 |
| 531 | Janno/Bachelor-Thesis | Constructive Theory of Regular Languages | 2 |
| 532 | supercooldave/ruse | Ruse programming language. | 2 |
| 533 | AdaCore/sparkformal | The project SPARK Formal aims at developing a complete semantics of the SPARK language in Coq. | 2 |
| 534 | arthuraa/coq-utils | Some basic libraries for Coq. | 2 |
| 535 | mcopes73/FTA | Complete formalization of the Fundamental Theorem of Arithmetic in Coq and Isabelle/HOL. | 2 |
| 536 | coq-contribs/continuations | A toolkit to reason with programs raising exceptions | 2 |
| 537 | coq-contribs/ramsey | Ramsey Theory | 2 |
| 538 | lucaspena/coinduction | 2 | |
| 539 | pnwamk/strands | Embedding strand spaces in Coq and working to verify correctness and other properties. | 2 |
| 540 | mwand/MPCF | 2 | |
| 541 | coreyoconnor/learn-coq | various exercises I've worked through (or failed to work through) while learning the proof assistant Coq. | 2 |
| 542 | cmc333333/forensics-thesis-code | Accompanying Code for Depaul Thesis | 2 |
| 543 | wilcoxjay/notes | 2 | |
| 544 | michaelsproul/dblib-linear | Formalisation of the linear lambda calculus in Coq | 2 |
| 545 | amintimany/UniverseComparator | A tool to compare universe levels in Coq. | 2 |
| 546 | hide-kawabata/traf | A proof tree viewer that works with Coq through Proof General | 2 |
| 547 | ppedrot/issection-tactic | A Coq tactic checking whether a variable is a section variable or not | 2 |
| 548 | shimomura1004/coqle | 2 | |
| 549 | master-q/coqtactic-injectfalse | Custom tactic named "ij_injectfalse" injects False into the hypothesis | 2 |
| 550 | simonr89/SyDRec | A module for the inductive theorem prover Coq, which generates function and theorems based on inductive type definitions. | 2 |
| 551 | davidnowak/cecoa | Implicit-complexity Coq library to prove that some programs are computable in polynomial time | 2 |
| 552 | thery/grobner | A fornalisation of Grobner basis in ssreflect | 2 |
| 553 | G33KatWork/Nexys3_PSRAM | An implementation of a synchronous PSRAM controller on a Nexys 3 FPGA board. There certainly is room for improvement, but it does 64bit read- and write-bursts for now with fixed latency. | 2 |
| 554 | verimath/topology | Zorn's Lemma and General Topology | 2 |
| 555 | coq-contribs/paradoxes | Paradoxes in Set Theory and Type Theory | 2 |
| 556 | thery/coqprime | Prime numbers for Coq | 2 |
| 557 | chiragbharadwaj/learning-coq | Learning Coq by following the classic "Software Foundations" texts. | 2 |
| 558 | myuon/CatQ | Formalization of Setoids-enriched Category Theory | 2 |
| 559 | finrod/Refocusing | A formalisation of the refocusing transformation by Danvy et al. in Coq | 2 |
| 560 | coq-contribs/coqoban | Sokoban (in Coq) | 2 |
| 561 | rouanth/learning | Various completely useless projects | 2 |
| 562 | kisom/okasaki-coq | Coq definitions of the data structures in PFDS. | 2 |
| 563 | tchajed/cardinality | Reasoning about finite type cardinality in Coq | 2 |
| 564 | UniMath/lBsystems | Voevodsky's work on B-systems, transferred from his github account | 2 |
| 565 | bollu/propogators-coq | A formalisation of propogators as ekmett speaks about them on the livestream: https://www.twitch.tv/ekmett | 2 |
| 566 | folone/sf-building | An attempt to compile and generate docs from Benjamin Pierce's "Software Foundations" | 2 |
| 567 | frenetic-lang/featherweight-openflow | 2 | |
| 568 | hephaestus-pl/coqffj | 2 | |
| 569 | lematt1991/ICFP15-Coq-Proofs | Proofs of correctness for "Partial Aborts for Software Transactional Memory" formalized in Coq | 2 |
| 570 | khibino/CoPL-read | 2 | |
| 571 | snu-sf/cpdtlib | 2 | |
| 572 | mathink/mslambda | Map, Skeleton, Lambda term. | 2 |
| 573 | stelleg/cem_coq | Coq implemenation of CEM with proof of correctness | 2 |
| 574 | CoqHott/univalent_parametricity | Univalent Parametricity for Effective Transport | 2 |
| 575 | ymanerka/pipeproof | PipeProof | 2 |
| 576 | secworks/hc | Hardware implementation of the HC stream cipher. | 2 |
| 577 | daeseoklee/kaist-coq-study---real-number-construction | 2 | |
| 578 | sayon/coq-cata | study on coq catamorphisms encoding | 2 |
| 579 | coq-io/opam-website | Generation of a sample Coq website for OPAM | 2 |
| 580 | samchrisinger/uttsolver | An ultimate tic tac toe solver written in coq and compiled to haskell | 2 |
| 581 | ml4tp/tcoq | Modification to Coq to record intermediate proof states encountered during a proof | 2 |
| 582 | slasser/vermillion | LL(1) parser generator verified in Coq | 2 |
| 583 | coq-contribs/euclidean-geometry | Basis of the Euclid's plane geometry | 2 |
| 584 | coq-contribs/random | Interpretation of random programs | 2 |
| 585 | aa755/SquiggleEq | 2 | |
| 586 | andrewtron3000/shannon-coq | 2 | |
| 587 | SkySkimmer/NormalisationByCompleteness | 2 | |
| 588 | beta-ziliani/mtac-plugin | Plugin for Coq 8.5 | 2 |
| 589 | Choibrian25/Arithmetic_Logic_Unit.V | This is a basic ALU created in Verilog. This was initially created for ECE 324-"Digital Design" taught by Tom Pritchard and is expanded on as an extracurricular project. | 2 |
| 590 | yoshihiro503/gbasen | Generalized Base-N encoding and decoding | 2 |
| 591 | domdere/haskell-coq | Common Haskell type classes written up in the Coq (GALLINA) theorem prover language for proving properties about Haskell data types and functions [Coq] | 2 |
| 592 | benediktahrens/rezk_completion | Rezk completion | 2 |
| 593 | drouhling/LaSalle | A formal proof of LaSalle's invariance principle | 2 |
| 594 | nmvdw/HITs-Examples | Examples of Higher Inductive Types | 2 |
| 595 | asr/tm-coinduction | 2 | |
| 596 | olaure01/yalla | Yet Another deep embedding of Linear Logic in Coq | 2 |
| 597 | Chobbes/Coqplexity | Reasoning about complexity classes in Coq with Coquelicot | 2 |
| 598 | mkolosick/Software-Foundations-Exercises | Exercises in Software Foundations | 2 |
| 599 | jeapostrophe/redex | redex modules for papers, etc | 2 |
| 600 | pilki/cases | A bit more than the (S*)Case tactics in Coq | 2 |
| 601 | dredozubov/sf | Software foundation exercises | 2 |
| 602 | ashwith/hdlroot | root directory for my Verilog/VHDL files | 2 |
| 603 | unaoya/sou-ken-topos | 2 | |
| 604 | JasonGross/coq-scripts | Various useful scripts for dealing with Coq files | 2 |
| 605 | fsq/CS386L-Programming-Language | CS386L Programming Language assignments | 2 |
| 606 | jefflieu/fpga | Collection of small but useful HDL cores | 2 |
| 607 | wilcoxjay/miniprl-coq | A port of MiniPRL to Coq | 2 |
| 608 | nmpgaspar/Mefresa | A Mechanized Framework for Reasoning on Software Architectures | 2 |
| 609 | thery/Plouffe | Computing Pi decimal using Plouffe Formula in Coq | 2 |
| 610 | beta-ziliani/sf | Software Foundations of Pierce et al. | 2 |
| 611 | kisom/vlisp | Experiments building a formally-verified Lisp. | 2 |
| 612 | jwiegley/vfa | 2 | |
| 613 | cmcl/msci | MSci project: Development of a formalisation of "Propositions as Sessions" | 2 |
| 614 | coq-io/lwt | Lwt back-end for Coq.io. | 2 |
| 615 | goldfirere/cs231 | Course materials for Bryn Mawr's CS231: Discrete Math | 2 |
| 616 | gstew5/games | 2 | |
| 617 | cogumbreiro/habanero-coq | Coq formalization of the Habanero programming model. | 2 |
| 618 | erikmd/ssr-under-tac | A tactic to rewrite under lambdas in SSReflect/MathComp | 2 |
| 619 | Barry-Jay/Intensional-computation | translations of a lambda abstraction to combinations of operators | 2 |
| 620 | sec-bit/calculus-token-with-proof | 2 | |
| 621 | catalin-hritcu/exos-ssr | Solving exercises for SSReflect tutorial from Sept 2010 | 2 |
| 622 | verimath/real | Real Numbers as CoInductive Streams of Digits | 2 |
| 623 | jashug/IWTypes | A Coq development of the theory of Indexed W types with function extensionality. | 2 |
| 624 | wilcoxjay/mechanized-metatheory2 | 2 | |
| 625 | coq-contribs/miniml | Correctness of the compilation of Mini-ML into the Categorical Abstract Machine | 2 |
| 626 | letouzey/hofstadter_g | Coq proofs about Hofstadter's function G | 2 |
| 627 | nmvdw/groupoids | Groupoids vs 1-Types | 2 |
| 628 | Formal-Systems-Laboratory/coinduction | language-independent program verification by coinduction | 2 |
| 629 | coq-contribs/icharate | A logical Toolkit for Multimodal Categorial Grammars | 2 |
| 630 | ejgallego/ssrbit | A small library for Bit Sequences | 2 |
| 631 | yforster/stlc-norm | Proof that STLC is normalizing in Fstar | 2 |
| 632 | skeuchel/gdtc | 2 | |
| 633 | ppedrot/ll-coq | Some Coq formalizations of Linear Logic | 2 |
| 634 | DanGrayson/Ktheory | formalization of theorems of higher algebraic K-theory | 2 |
| 635 | aslanix/SmallStepNI | Mechanization of a noninterference proof for a toy imperative language with small-step semantics in Coq | 2 |
| 636 | jhuapl-saralab/slmech | 2 | |
| 637 | PierreLescanne/DependentTypesForExtensiveGames | In this repository I present a Coq developement of extensive games using dependent types, together with examples | 2 |
| 638 | reservoirlabs/rcoqlib | R-CoqLib: general-purpose Coq libraries and tactics | 2 |
| 639 | jwiegley/tactics | A place to collect small, random, useful tactics (that probably exist many other places) | 2 |
| 640 | JoeyEremondi/vscode-ott | Ott Support for Visual Studio Code | 2 |
| 641 | coq-contribs/hoare-tut | A Tutorial on Reflecting in Coq the generation of Hoare proof obligations | 2 |
| 642 | mrhaandi/ipc2 | Reduction from Diophantine equations to provability in IPC2 / System F. | 2 |
| 643 | shengfeng/formalization_of_MDESL | Formalization of MDESL | 2 |
Inspired by awesome repo rxjs-ecosystem. Thanks Nick