Awesome Coq

Description:
Awesome Coq is a curated directory of Coq libraries, plugins, tools, verification projects, and learning resources for the Coq proof assistant and interactive theorem proving.

Website: https://github.com/coq-community/awesome-coq#readme

Category: Themed directories
Tags: awesome-lists, developer-resources

---

Features

• Comprehensive curated list

  • Collects Coq-related projects and resources in a single, organized index.
  • Focuses on items relevant to interactive theorem proving and formal verification.

• Project categories

  • Frameworks – general frameworks and ecosystems built on top of Coq.
  • User Interfaces – front-ends and UI tools that improve the Coq interaction experience.
  • Libraries – reusable Coq libraries for mathematics, data structures, algorithms, and other domains.
  • Package and Build Management – tools and infrastructure for packaging, building, and managing Coq projects.
  • Plugins – Coq extensions and plugins that add or modify proof engine capabilities.
  • Puzzles and Games – Coq-based puzzles, games, and interactive or educational examples.
  • Tools – auxiliary tools that assist in Coq development, maintenance, and refactoring, such as:
    • find-bug.py
    • absolutize-imports.py
    • inline-imports.py
    • minimize-requires.py
    • move-requires.py
    • move-vernaculars.py
    • proof-using-helper.py
  • Type Theory and Mathematics – formalizations in logic, type theory, and mathematics.
  • Verified Software – projects applying Coq to software verification and certified systems.

• Learning and community resources

  • Community – links to community hubs and communication channels around Coq.
  • Blogs – blog posts and series related to Coq and formal methods.
  • Books – textbooks and longer-form written material for learning Coq.
  • Course Material – lecture notes, assignments, and course repositories that teach Coq.
  • Tutorials and Hints – beginner to advanced tutorials, tips, and guidance for proof development.

• Open contribution model

  • Public contribution guidelines for suggesting new entries or improvements.
  • Maintained under the coq-community organization.

• Open license

  • Distributed with a LICENSE file (open-source license; see repository for exact terms).

---

Target Use Cases

• Discovering Coq libraries, plugins, and tools for new or existing projects.
• Finding verified software and large-scale formalization efforts in Coq.
• Locating educational materials for teaching or learning Coq.
• Exploring the Coq ecosystem via categorized links instead of ad-hoc searches.

---

Pricing

• Not a commercial product or service.
• Public GitHub directory; access and usage are free.