Coq

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

0

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

Development of homotopy-theoretic ideas.
0

UniMath github.com
tool category #coq link ↗

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

Sail github.com
tool category #coq link ↗

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

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

Cryptographic primitive code generation.
0

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

Axiom-free formalization of category theory.
0

Cosette github.com
tool category #coq link ↗

Automated solver for reasoning about SQL query equivalences.
0

Verdi github.com
tool category #coq link ↗

Framework for formally verifying distributed systems implementations.
0

MetaCoq github.com
tool category #coq link ↗

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

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

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

jsCoq github.com
tool category #coq link ↗

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

VsCoq github.com
tool category #coq link ↗

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

Ott github.com
tool category #coq link ↗

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

Jasmin github.com
tool category #coq link ↗

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

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

IDE extensions for Proof General's Coq mode.
0

Coqtail github.com
tool category #coq link ↗

Interface for Coq based on the Vim text editor.
0

Alectryon github.com
tool category #coq link ↗

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

QuickChick github.com
tool category #coq link ↗

Plugin for randomized property-based testing.
0

CoqOfOCaml github.com
tool category #coq link ↗

Tool for generating idiomatic Coq from OCaml code.
0

Interaction Trees github.com
tool category #coq link ↗

Library for representing recursive and impure programs.
0

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

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

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.
0

Analysis github.com
tool category #coq link ↗

Library for classical real analysis compatible with Mathematical Components.
0

Coq Platform github.com
tool category #coq link ↗

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

Equations github.com
tool category #coq link ↗

Function definition package for Coq.
0

GeoCoq github.com
tool category #coq link ↗

Formalization of geometry based on Tarski's axiom system.
0

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.
0

JSCert github.com
tool category #coq link ↗

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

Verdi Raft github.com
tool category #coq link ↗

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

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

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

CertiCoq github.com
tool category #coq link ↗

Verified compiler from Gallina, the internal language of Coq, down to CompCert's Clight language.
next page of items loading…