falso
Proof technique
An implementation of a proof technique in the Coq proof assistant that exploits a bug to demonstrate the existence of a false statement
A proof of false in Coq.
93 stars
5 watching
1 forks
Language: Coq
last commit: about 5 years ago Related projects:
| Repository | Description | Stars |
|---|---|---|
 coq/platform | A multi-platform distribution of the Coq proof assistant and its libraries, providing a standardized setup for development and teaching | 188 |
 uwplse/structtact | A Coq library providing structural tactics and utility definitions to simplify proof development in proof assistants. | 21 |
 formal-land/coq-of-rust | Tool that verifies Rust code by translating it into Coq's proof system to ensure no bugs or vulnerabilities exist | 421 |
 thery/flocqlecture | An introductory course on formalizing floating-point numbers and their applications in Coq | 6 |
 stepchowfun/proofs | A personal repository of formally verified mathematics using the Coq proof assistant | 291 |
 engineeringsoftware/mcoq | Analyze and test Coq proof assistant projects by generating modified versions of the code to identify flaws in specifications. | 30 |
 coq-community/coq-art | Coq proof assistant book with exercises and examples | 110 |
| coq-community/fourcolor | A formal proof of a fundamental result in graph theory using the Coq proof assistant | 166 |
 matafou/libhyps | A Coq library providing tactics to manipulate hypotheses in formal proofs. | 20 |
 ejgallego/coq-lsp | A tool for interactive theorem proving and language support in Coq | 152 |
 jasongross/coq-tools | Tools for helping find and fix bugs in the Coq proof assistant development environment. | 39 |
 impermeable/coq-waterproof | Helps write formal proofs in a more readable format | 33 |
 rafaelcgs10/w-in-coq | A Coq formalization of Damas-Milner type system and its algorithm W for verifying the correctness of type inference tools. | 25 |
 lukaszcz/coqhammer | A tool for automating proof search and verification in dependent type theory using machine learning and external provers. | 218 |