Git Product home page Git Product logo

coq-community's Projects

aac-tactics icon aac-tactics

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

alea icon alea

Coq library for reasoning on randomized algorithms [maintainers=@anton-trunov,@volodeyka]

almost-full icon almost-full

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

apery icon apery

A formal proof of the irrationality of zeta(3), the Apéry constant [maintainer=@amahboubi,@pi8027]

atbr icon atbr

Coq library and tactic for deciding Kleene algebras [maintainer=@tchajed]

autosubst icon autosubst

Automation for de Bruijn syntax and substitution in Coq [maintainers=@RalfJung,@co-dan]

awesome-coq icon awesome-coq

A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainer=@palmskog]

bertrand icon bertrand

Coq proof of Bertrand's postulate on existence of primes [maintainer=@thery]

bignums icon bignums

Coq library of arbitrarily large numbers, providing BigN, BigZ, BigQ that used to be part of the standard library [maintainers=@proux01,@erikmd]

bits icon bits

A formalization of bitset operations in Coq and the corresponding axiomatization and extraction to OCaml native integers [maintainer=@anton-trunov]

buchberger icon buchberger

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

chapar icon chapar

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

comp-dec-modal icon comp-dec-modal

Completeness and Decidability of Modal Logic Calculi [maintainer=@chdoc]

coq-art icon coq-art

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

coq-dpdgraph icon coq-dpdgraph

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

coq-ext-lib icon coq-ext-lib

A library of Coq definitions, theorems, and tactics. [maintainers=@gmalecha,@liyishuai]

coq-nix-toolbox icon coq-nix-toolbox

Nix helper scripts to automate local builds and CI [maintainers=@CohenCyril,@Zimmi48]

coq-performance-tests icon coq-performance-tests

A library of Coq source files testing for performance regressions on Coq [maintainer=@JasonGross]

coq-plugin-template icon coq-plugin-template

Template project for Coq plugins using the Dune build system, showcasing some advanced features [maintainer=@ejgallego]

coq-program-verification-template icon coq-program-verification-template

Template project for program verification in Coq, showcasing reasoning on CompCert's Clight language using the Verified Software Toolchain [maintainer=@palmskog]

coq-tricks icon coq-tricks

Tricks you wish the Coq manual told you [maintainer=@tchajed]

coqdocjs icon coqdocjs

Collection of scripts to improve the output of coqdoc [maintainers=@chdoc,@palmskog]

coqeal icon coqeal

The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]

coqffi icon coqffi

Automatically generates Coq FFI bindings to OCaml libraries [maintainer=@lthms]

coqoban icon coqoban

Sokoban (in Coq) [maintainer=@erikmd]

coqtail-math icon coqtail-math

Coqtail is a library of mathematical theorems and tools proved inside the Coq proof assistant. Results range mostly from arithmetic to real and complex analysis. [maintainer=@jmadiot]

corn icon corn

Coq Repository at Nijmegen [maintainers=@spitters,@VincentSe,@Lysxia]

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.