#

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

dc-mak / coq-dpdgraph

Build dependency graphs between COQ objects

neo4j graph coq coq-plugin

Updated Dec 2, 2017
HTML

meduzik / software-foundations-ru

Russian Translation for Software Foundations book.

translation coq software-foundations

Updated Feb 23, 2018
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

clarus / coq-blog

A blog about Coq

coq

Updated Mar 21, 2021
HTML

racherb / racherb.github.io

✨ racherb's personal blog

blog haskell functional-programming coq artificial-intelligence safety ethical

Updated Apr 2, 2021
HTML

anton-trunov / ssreflect-london-tydd-meetup

SSReflect talk at London Type-Driven Development meetup

coq ssreflect mathcomp

Updated Apr 20, 2021
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

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

Coq-zh / SF-zh

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

translation coq chinese-translation

Updated Mar 14, 2022
HTML

composarc / sf-zh

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

coq zh-cn traduction

Updated Mar 14, 2022
HTML

ahmedishraq / CSE460-Lab

CSE460 - VLSI Design

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

Updated Feb 9, 2023
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

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

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

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

rocq-community / rocq-community.github.io

Rocq-community website

website coq rocq-prover

Updated Mar 27, 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

aibolem / rocq-art-welle

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

coq rocq

Updated May 26, 2025
HTML

Created by Gérard Pierre Huet, Thierry Coquand

Released 1989

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