Explore projects

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.

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

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

This repository contains the Coq/Iris proofs that accompany the paper Spy game---Verifying a local generic solver in Iris

"Static Analysis for Optimizing Compilers" master course supports

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

Abstract Interpretation with ITrees.

Itauto: an Extensible Intuitionistic SAT Solver

Itauto: an Extensible Intuitionistic SAT Solver

Separation Logic with Characteristic Formulae Entirely within Coq

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

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.