Starred repositories
12
stars
written in Rocq Prover
Clear filter
A Learning Environment for Theorem Proving with the Coq proof assistant
A library of mechanised undecidability proofs in the Coq proof assistant.
Coq code and exercises from the Coq'Art book [maintainers=@ybertot,@Casteran]
Modeling and Proving in Computational Type Theory
Libraries demonstrating design patterns for programming and proving with canonical structures in Coq [maintainer=@anton-trunov]
A Coq formalization of the textbook Categories and Toposes: Visualized and Explained
Coq development accompanying the LFCS'22 paper "Constructive and Mechanised Meta-Theory of Intuitionistic Epistemic Logic"