Explore projects

Mirror for CI/CD purposes only.

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

A Coq tactic for discharging goals about floating-point arithmetic and round-off errors using the Gappa prover.

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

Itauto: an Extensible Intuitionistic SAT Solver

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.

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

CompCertSSA is built on top of the C CompCert verified compiler. It adds an SSA-based middle-end at the RTL level, and includes conversion to SSA, SSA-based optimizations, and destruction of SSA.

An LR(1) parser generator for OCaml.

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.

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

This repository contains the Coq/Iris proofs that accompany the paper A Separation Logic for Effect Handlers.

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