#

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...

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

aibolem / rocq-art-welle

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

coq rocq

Updated May 26, 2025
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

racherb / racherb.github.io

✨ racherb's personal blog

blog haskell functional-programming coq artificial-intelligence safety ethical

Updated Apr 2, 2021
HTML

composarc / sf-zh

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

coq zh-cn traduction

Updated Mar 14, 2022
HTML

dc-mak / coq-dpdgraph

Build dependency graphs between COQ objects

neo4j graph coq coq-plugin

Updated Dec 2, 2017
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

FedericoBruzzone / software-foundations

Solutions (in Coq) of the exercises in the software foundation books.

functional-programming ocaml coq software-foundations coq-library

Updated Aug 12, 2024
HTML

jaalonso / jaalonso.github.io

Índice de repositorios.

haskell functional-programming coq prolog proof-assistant lean logic-programming isabelle

Updated Dec 16, 2025
HTML

RvnKali / Prime-Numbers

# Prime-Numbers Web AppThis web app helps users explore prime numbers through features like checking primality and generating sequences. With clear visuals and step-by-step explanations, it makes understanding prime numbers simple and engaging. 🐙✨

rust verify benchmark cryptography generator random safe-prime coq bignum theorem-proving multithreading ctf num prime-factors primes num-traits num-bigint generating-primes

Updated Dec 17, 2025
HTML

h2-math / coq-nahas-tutorial

Coq Tutorial from Mike Nahas's repo at https://github.com/mdnahas/mdnahas.github.io/doc/nahas_tutorial.v

math coq logic proof-assistant interactive-theorem-proving

Updated Jan 15, 2025
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

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

Created by Gérard Pierre Huet, Thierry Coquand

Released 1989

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