Repository navigation
Coq
Created by Gérard Pierre Huet, Thierry Coquand
发布于 1989
- Repository
- coq/coq
- Website
- coq.inria.fr
- Wikipedia
- 维基百科
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.
The Rocq Prover is an interactive theorem prover, or proof assistant. 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.
This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.
Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make super safe applications! ✈️ 🚀 ⚕️ 🏦
《软件基础》中译版 Software Foundations Chinese Translation
A dependently-typed proof language intended to make provably correct bare metal code possible for working software engineers.
An axiom-free formalization of category theory in Coq for personal study and practical work
A framework for formally verifying distributed systems implementations in Coq
A gently curated list of companies using verification formal methods in industry
A port of Coq to Javascript -- Run Coq in your Browser
This repo is the new home of Proof General
Tricks you wish the Coq manual told you [maintainer=@tchajed]
Verified Software Toolchain
Metaprogramming, verified meta-theory and implementation of Rocq in Rocq
Visual Studio Code extension for Coq
A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainer=@palmskog]
A verification toolchain for Rust programs