A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]

The CompCert formally-verified C compiler

An axiom-free formalization of category theory in Coq for personal study and practical work

A library of mechanised undecidability proofs in the Coq proof assistant.

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

A library for formalizing Haskell types and functions in Coq

Brainfuck formalized in Coq

This repo keeps track of my codes, answers and thinkings when exploring books.

Convert Haskell source code to Coq source code

🐣 A blog engine written and proven in Coq

A proof of false in Coq.

Writeup that goes along with this: