Select a tag to browse associated projects and drill deeper into the tag cloud.
Coq proof assistant
Analyzed 12 months ago
Coq is a formal proof management system: a proof done with Coq is mechanically checked by the machine. In particular, Coq allows:
* to define functions or predicates,
* to state mathematical theorems and software specifications,
* to develop interactively formal proofs of these theorems,
* to
Licenses:
lgpl
learn-haskell-coq-ml-etc
L
Analyzed 12 months ago
Where I try code from Haskell (etc) books, articles, etc.
Licenses:
No declared licenses
CompCert
C
Analyzed 12 months ago
The CompCert project investigates the formal verification of realistic compilers usable for critical embedded software. Such verified compilers come with a mathematical, machine-checked proof that the generated executable code behaves exactly as prescribed by the semantics of the source program. By
Licenses:
No declared licenses
Mathematical Components (Coq)
M
Analyzed 12 months ago
Mathematical Components are libraries of formalized mathematics developed using the Coq proof assistant. This project finds its roots in the formal proof of the Four Color Theorem. It has been used for large scale formalization projects, including a formal proof of the Odd Order (Feit-Thompson)
Licenses:
cecill_b
Coq ELPI
C
Analyzed 12 months ago
Coq-Elpi provides a Coq plugin that lets one define new commands and tactics in Elpi (Embeddable λProlog Interpreter). For that purpose it provides an embedding of Coq's terms into λProlog using the Higher-Order Abstract Syntax approach (HOAS). It also exports to Elpi a comprehensive set of Coq's
Licenses:
No declared licenses
Flocq
F
No analysis available
Flocq (Floats for Coq) is a floating-point formalization for the Coq system. It provides a comprehensive library of theorems on a multi-radix multi-precision arithmetic. It also supports efficient numerical computations inside Coq.
Mostly written in language not available
Licenses:
lgpv3_or_...
software-foundations
S
Analyzed 12 months ago
Software Foundations in Idris
Licenses:
No declared licenses
Interval Package for Coq
I
No analysis available
This library provides vernacular files containing tactics for simplifying the proofs of inequalities on expressions of real numbers for the Coq proof assistant.
Mostly written in language not available
Licenses:
lgpl21
iron lambda
I
Analyzed 12 months ago
Coq formalizations of functional languages
Licenses:
No declared licenses