Explore projects

Separation Logic with Characteristic Formulae Entirely within Coq

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

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.

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

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

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.

Formalizations accompanying my thesis "Extending Type Theory with Syntactical Models".

Coq files related to skeletons

A 3 hour and a half tutorial for the Coq system

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

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

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

Dijkstra monads and effect observations

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

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

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.

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