Between 2021 and 2023, I developped on the open-source Frama-C software which gives a framework for combining different formal methods for verifying C programs. I mostly work in the E-ACSL plugin dedicated to runtime assertion checking. My work in this plugin consists in improving on the performance of the generated code, especially for arithmetic annotations in the presence of logic functions via a static analysis. This analysis based on interval arithmetic is quite involved when recursive functions are used.

CaTT is a dependent type theory whose models are the weak ω-categories. It is implemented in OCaml and I also host an interactive online version available for quick tests

An Agda formalization of the type theory CaTT, as a special case of a framework that I call free globular type theories. This provides a certified interpreter for the bare language CaTT (without syntactic sugar), as well as a setup to prove properties such as decidability of type checking, uniqueness of derivations, and all the lemma on which the categorical analysis of the theory relies.

During a research internship under the supervision of Florent Hivert, I have formalized the computation of the representations of the symmetric groups and their characters using Young tableaux, in Coq with ssreflect (now MathComp). This project has been integrated into Florent’s development of algebraic combinatorics.

Here you can find the source files and the script we used to benchmark the article on abstract interpretation of recursive function in E-ACSL, along with the version of Frama-C and E-ACSL that we ran the benchmarks on.

An emulator for the i8080 chip and the space invaders arcade machine written in OCaml.