Trending
See what the GitHub community is most excited about this month.
-
Homotopy type theory
-
This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
-
Metaprogramming in Coq
-
Tricks you wish the Coq manual told you
-
A Library for Representing Recursive and Impure Programs in Coq
-
Convert Haskell source code to Coq source code
-
Verified Software Toolchain
-
Mathematical Components
-
The CompCert formally-verified C compiler
-
An axiom-free formalization of category theory in Coq for personal study and practical work
-
A framework for formally verifying distributed systems implementations in Coq
-
Formal Reasoning About Programs
-
Voevodsky's original development of the univalent foundations of mathematics in Coq
-
FSCQ is a certified file system written and proven in Coq
-
A Coq specification of ECMAScript 5 (JavaScript) with verified reference interpreter
-
A blog engine written and proven in Coq.
-
Randomized Property-Based Testing Plugin for Coq
-
Advent of Code 2018, in Coq! (https://adventofcode.com/2018)
-
Cryptographic Primitive Code Generation by Fiat
-
A library for formalizing Haskell types and functions in Coq
-
The Vellvm II coq development.
-
A selection of formal developments in Coq.
-
Mindless, verified (erasably) coding using dependent types
-
A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters]
-
An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
