My works of mathematical proof using functional languages

Proof that the FFT implements the DFT, written in Coq.

[WORK IN PROGRESS] Mechanized Proof for Article: "Memento: A Framework for Detectable Recoverability in Persistent Memory" (PLDI 2023)

An implementation of the IMP language in Coq with two proofs.

Various sorting algorithms formalised using the "sauto" component of CoqHammer 1.3.

A small coq library for verifying OCaml native integer computations

Coq programs made during my Bachelor's Degree at the University of Lyon in France.

Coq proof of an equivalence relation that is not congruent on the Imp language from Software Foundations

BFS and DFS proofs for Coq.

A verified system transformer for serialization of Verdi systems using the Cheerios library.

Proofs of correctness for "Partial Aborts for Software Transactional Memory" formalized in Coq

Change impact analysis in Coq and OCaml

Mechanized Proof for Article: "Revamping Hardware Persistency Models: View-Based and Axiomatic Persistency Models for Intel-x86 and Armv8" (PLDI 2021)

Formal proof that closure conversion with flat environments is safe for space.

Software Foundations is a broad introduction to the mathematical underpinnings of reliable software.

He Reiter, Ho Reiter, He Reiter, Immer weiter!

Formalisation of the linear lambda calculus in Coq

Lens, State is your father... and I can prove It!