Explore projects

A small Coq proof for an exercise that was probably taken from the mathematical olympiads

Tutorial for CFML 2.0

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

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.

Formally verified ML implementation of Knuth's Dancing Links algorithm, using CFML.

Backup of Cocorico, the Coq wiki, now hosted at https://github.com/coq/coq/wiki Synchronized with github every hour

A 3 hour and a half tutorial for the Coq system

Squelette utilisé dans un cours de preuves formelles donné aux jncf 2018

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

Providing comparison functions between numbers that are sums of a rational number and a square root, with proofs in Coq+mathematlcal components

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

Files for the course at EJCP 2019

Formal operational semantic of WEBI language written in coq. Purpose of this project is to give a behavioural description of WEBI in COQ, using Small Step and Skeletal Semantics