Explore projects

GitLab mirror of https://github.com/math-comp/math-comp

Mirror for CI/CD purposes only.

Why3 is a software verification platform, featuring a versatile ML-style language and interfaces to various powerful automated and interactive theorem provers.

Resources for course MPRI 2-4 on functional programming and type systems.

Itauto: an Extensible Intuitionistic SAT Solver

Apps to compile from skel to gallina for use with the Coq Proof Assistant

CertrBPF: a fully verified RIOT rBPF (verifier+interpreter+JIT) in Coq

Dépôt git pour le site web de Liber Abaci

implementation and metatheory of time credits and time receipts in Iris / Coq

Separation Logic with Characteristic Formulae Entirely within Coq

CoqInterval provides tactics for simplifying the proofs of inequalities on expressions of real numbers for the Coq proof assistant.

A Coq formalization of real analysis compatible with the standard library.

A Coq formalization of real analysis compatible with the standard library.