Software development

Research related contribution


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- An infinity categorical coherence typechecker

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.

Formalization of representation of symmetric groups

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.

Artifacts for submitted articles

Benchmark for abstract interpretation of recursive functions in E-ACSL

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.

benchmarks frama-c/e-acsl

Other contribution


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