dogear

enter for all results · esc to close

Coq

215 items from coq-community/awesome-coq ★396

tools
  1. Homotopy Type Theory github.com
    tool category #coq link ↗

    Development of homotopy-theoretic ideas.

  2. UniMath github.com
    tool category #coq link ↗

    Library which aims to formalize a substantial body of mathematics using the univalent point of view.

  3. Sail github.com
    tool category #coq link ↗

    Tool for specifying instruction set architecture (ISA) semantics of processors and generating Coq definitions.

  4. Fiat-Crypto github.com
    tool category #coq link ↗

    Cryptographic primitive code generation.

  5. Category Theory in Coq github.com
    tool category #coq link ↗

    Axiom-free formalization of category theory.

  6. Cosette github.com
    tool category #coq link ↗

    Automated solver for reasoning about SQL query equivalences.

  7. Verdi github.com
    tool category #coq link ↗

    Framework for formally verifying distributed systems implementations.

  8. MetaCoq github.com
    tool category #coq link ↗

    Project formalizing Coq in Coq and providing tools for manipulating Coq terms and developing certified plugins.

  9. Tricks in Coq github.com
    tool category #coq link ↗

    Tips, tricks, and features in Coq that are hard to discover.

  10. jsCoq github.com
    tool category #coq link ↗

    Port of Coq to JavaScript, which enables running Coq projects in a browser.

  11. VsCoq github.com
    tool category #coq link ↗

    Language server and extension for the Visual Studio Code and VSCodium editors.

  12. Ott github.com
    tool category #coq link ↗

    Tool for writing definitions of programming languages and calculi that can be translated to Coq.

  13. Jasmin github.com
    tool category #coq link ↗

    Formalized language and verified compiler for high-assurance and high-speed cryptography.

  14. Company-Coq github.com
    tool category #coq link ↗

    IDE extensions for Proof General's Coq mode.

  15. Coqtail github.com
    tool category #coq link ↗

    Interface for Coq based on the Vim text editor.

  16. Alectryon github.com
    tool category #coq link ↗

    Collection of tools for writing technical documents that mix Coq code and prose.

  17. QuickChick github.com
    tool category #coq link ↗

    Plugin for randomized property-based testing.

  18. CoqOfOCaml github.com
    tool category #coq link ↗

    Tool for generating idiomatic Coq from OCaml code.

  19. Interaction Trees github.com
    tool category #coq link ↗

    Library for representing recursive and impure programs.

  20. Four Color Theorem github.com
    tool category #coq link ↗

    Formal proof of the Four Color Theorem, a landmark result of graph theory.

  21. CoqHammer github.com
    tool category #coq link ↗

    General-purpose automated reasoning hammer tool that combines learning from previous proofs with the translation of problems to automated provers and the reconstruction of found proofs.

  22. Analysis github.com
    tool category #coq link ↗

    Library for classical real analysis compatible with Mathematical Components.

  23. Coq Platform github.com
    tool category #coq link ↗

    Curated collection of packages to support Coq use in industry, education, and research.

  24. Equations github.com
    tool category #coq link ↗

    Function definition package for Coq.

  25. GeoCoq github.com
    tool category #coq link ↗

    Formalization of geometry based on Tarski's axiom system.

  26. Coq LSP github.com
    tool category #coq link ↗

    Language server and extension for the Visual Studio Code and VSCodium editors with custom document checking engine.

  27. JSCert github.com
    tool category #coq link ↗

    Coq specification of ECMAScript 5 (JavaScript) with verified reference interpreter.

  28. Verdi Raft github.com
    tool category #coq link ↗

    Implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework.

  29. Coq-Elpi github.com
    tool category #coq link ↗

    Extension framework based on λProlog providing an extensive API to implement commands and tactics.

  30. CertiCoq github.com
    tool category #coq link ↗

    Verified compiler from Gallina, the internal language of Coq, down to CompCert's Clight language.

  31. next page of items loading…