Skip to content
#

Coq

coq logo

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 642 public repositories matching this topic...

Created by Gérard Pierre Huet, Thierry Coquand

Released 1989

Latest release 4 months ago

Followers
59 followers
Repository
coq/coq
Website
coq.inria.fr
Wikipedia
Wikipedia