Coq topic
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. Typical applications include the certification of properties of programming languages, the formalization of mathematics and teaching.
category-theory
An axiom-free formalization of category theory in Coq for personal study and practical work
csclub-coq-course-spring-2021
A course on formal verification at https://compsciclub.ru/en, Spring term 2021
coq-big-o
A general yet easy-to-use formalization of Big O, Big Theta, and more based on seminormed vector spaces.
pnp
Lecture notes for a short course on proving/programming in Coq via SSReflect.
coq-serapi
Coq Protocol Playground with Se(xp)rialization of Internal Structures.
company-coq
A Coq IDE build on top of Proof General's Coq mode
coq-program-verification-template
Template project for program verification in Coq, showcasing reasoning on CompCert's Clight language using the Verified Software Toolchain [maintainer=@palmskog]
bonak
🧊 An indexed construction of semi-simplicial and semi-cubical types
perennial
Verifying concurrent crash-safe systems