stepchowfun / Proofs
Licence: other
A selection of formal proofs in Coq.
Stars: ✭ 135
Labels
Projects that are alternatives of or similar to Proofs
Ttlite
A SuperCompiler for Martin-Löf's Type Theory
Stars: ✭ 94 (-30.37%)
Mutual labels: type-theory, coq
Formal Type Theory
Formalising Type Theory in a modular way for translations between type theories
Stars: ✭ 74 (-45.19%)
Mutual labels: type-theory, coq
Interactiontrees
A Library for Representing Recursive and Impure Programs in Coq
Stars: ✭ 133 (-1.48%)
Mutual labels: coq
Fiat
Mostly Automated Synthesis of Correct-by-Construction Programs
Stars: ✭ 119 (-11.85%)
Mutual labels: coq
Awesome Provable
A curated set of links to formal methods involving provable code.
Stars: ✭ 111 (-17.78%)
Mutual labels: coq
Coq Ext Lib
A library of Coq definitions, theorems, and tactics. [[email protected],@liyishuai]
Stars: ✭ 102 (-24.44%)
Mutual labels: coq
Geocoq
A formalization of geometry in Coq based on Tarski's axiom system
Stars: ✭ 128 (-5.19%)
Mutual labels: coq
Coq Serapi
Coq Protocol Playground with Se(xp)rialization of Internal Structures.
Stars: ✭ 87 (-35.56%)
Mutual labels: coq
Agda
Agda is a dependently typed programming language / interactive theorem prover.
Stars: ✭ 1,699 (+1158.52%)
Mutual labels: type-theory
Math Classes
A library of abstract interfaces for mathematical structures in Coq [[email protected]]
Stars: ✭ 133 (-1.48%)
Mutual labels: coq
Proofs
A selection of formal proofs in Coq.
Instructions
Make sure you have the dependencies listed below. Then you can run make to verify the proofs. You can also use make lint to invoke the linters. The build artifacts can be removed with make clean.
Dependencies
The build system depends on the following:
You also need the usual set of Unix tools, such as echo, find, etc.
Note that the project description data, including the texts, logos, images, and/or trademarks,
for each open source project belongs to its rightful owner.
If you wish to add or remove any projects, please contact us at [email protected].