Explore projects
-
Updated
-
-
Updated
-
Resources for course MPRI 2-4 on functional programming and type systems.
Updated -
Why3 / why3
GNU Lesser General Public License v2.1 onlyWhy3 is a software verification platform, featuring a versatile ML-style language and interfaces to various powerful automated and interactive theorem provers.
Updated -
-
Updated
-
CoqInterval / interval
CeCILL-C Free Software License AgreementCoqInterval provides tactics for simplifying the proofs of inequalities on expressions of real numbers for the Coq proof assistant.
Updated -
Updated
-
-
Apps to compile from skel to gallina for use with the Coq Proof Assistant
Updated -
YUAN Shenghao / CertrBPF
GNU General Public License v2.0 or laterCertrBPF: a fully verified RIOT rBPF (verifier+interpreter+JIT) in Coq
Updated -
-
Updated
-
MOINE Alexandre / dislog
MIT LicenseUpdated -
implementation and metatheory of time credits and time receipts in Iris / Coq
Updated -
YUAN Shenghao / CertrBPFOpt
GNU General Public License v2.0 or laterUpdated -
CHARGUERAUD Arthur / cfml2
Creative Commons Attribution 4.0 InternationalSeparation Logic with Characteristic Formulae Entirely within Coq
Updated -
A Coq formalization of real analysis compatible with the standard library.
Updated