Mentions légales du service
An LR(1) parser generator for OCaml.
Why3 is a software verification platform, featuring a versatile ML-style language and interfaces to various powerful automated and interactive theorem provers.
Mirror of the git repository of Coq now hosted at https://github.com/coq/coq (synchronized every 15min)
Formalization in Coq and Why3 of a theory about weak control dependence
Coherent predicates: translation validation of properties of various types of predicates at runtime, interfacing with SMTCoq for validation of SMT unsatisfiability certificates.
GitLab mirror of https://github.com/math-comp/math-comp
Itauto: an Extensible Intuitionistic SAT Solver