#

Coq

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.

Here are 24 public repositories matching this topic...

Coq-zh / SF-zh

《软件基础》中译版 Software Foundations Chinese Translation

translation coq chinese-translation

Updated Mar 14, 2022
HTML

rocq-community / coq-100-theorems

Statements of famous theorems proven in Coq [maintainer=@jmadiot]

coq theorems

Updated Jun 23, 2025
HTML

anton-trunov / csclub-coq-course-spring-2021

A course on formal verification at https://compsciclub.ru/en, Spring term 2021

course coq ssreflect mathcomp

Updated Feb 28, 2023
HTML

courses-at-nju-by-hfwei / problem-solving-class-coq

Rock on Coq for the Problem Solving Class at Nanjing University

tutorial coq theorem-proving proof-assistant classes formal-methods nanjing-university problem-solving-class

Updated Nov 13, 2019
HTML

alhassy / next-700-module-systems

PhD research ;; What's the difference between a typeclass/trait and a record/class/struct? Nothing really, or so I argue.

language haskell lisp emacs modules records ocaml metaprogramming coq agda phd typeclasses first-class-citizens canonical-structures

Updated Oct 24, 2021
HTML

rocq-community / rocq-community.github.io

Rocq-community website

website coq rocq-prover

Updated Mar 27, 2025
HTML

meduzik / software-foundations-ru

Russian Translation for Software Foundations book.

translation coq software-foundations

Updated Feb 23, 2018
HTML

clarus / coq-blog

A blog about Coq

coq

Updated Mar 21, 2021
HTML

Blaisorblade / dot-iris

Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris — Coq Formalization

paper coq type-theory coq-formalization coq-formalizations soundness dot-calculus

Updated Sep 17, 2025
HTML

anton-trunov / ssreflect-london-tydd-meetup

SSReflect talk at London Type-Driven Development meetup

coq ssreflect mathcomp

Updated Apr 20, 2021
HTML

pindaroso / software-foundations

Software Foundations book and exercises taken from https://www.cis.upenn.edu/~bcpierce/sf/current/index.html

haskell math book coq type-theory category-theory exercises

Updated Feb 24, 2017
HTML

ankitku / Twisted_Functor_Verification

coq functor monoid formalization action semidirectproduct

Updated May 29, 2017
HTML

JoJoDeveloping / ACP

My project for a course at Saarland University called "Advanced Coq Programming". My work is limited to the Reflection.v and GeneralReflection.v files, with some slight modifications in PA.v and ZF.v

coq coq-tactic

Updated Apr 28, 2021
HTML

dot-iris / dot-iris.github.io

GitHub Pages website for https://github.com/Blaisorblade/dot-iris.

coq type-theory coq-formalization dot-calculus

Updated Feb 19, 2025
HTML

ahmedishraq / CSE460-Lab

CSE460 - VLSI Design

vhdl coq verilog-hdl verilog-project vlsi-design bracucse460

Updated Feb 9, 2023
HTML

racherb / racherb.github.io

✨ racherb's personal blog

blog haskell functional-programming coq artificial-intelligence safety ethical

Updated Apr 2, 2021
HTML

gijs-pennings / rocq-wf-recursion

A tutorial on well-founded recursion in Rocq

tutorial coq quicksort recursion binary-search-tree gcd induction well-founded rocq

Updated May 25, 2025
HTML

dc-mak / coq-dpdgraph

Build dependency graphs between COQ objects

neo4j graph coq coq-plugin

Updated Dec 2, 2017
HTML

aibolem / rocq-art-welle

Rocq-community website http://rocq-community.org

coq rocq

Updated May 26, 2025
HTML

composarc / sf-zh

《软件基础》中译版 Software Foundations Chinese Translation

coq zh-cn traduction

Updated Mar 14, 2022
HTML

Created by Gérard Pierre Huet, Thierry Coquand

Released 1989

Followers: 62 followers
Repository: coq/coq
Website: github.com/topics/coq
Wikipedia: Wikipedia