I am a post-doctorate researcher at CEA LIST in the LSL team, and I work mainly on the plugin E-ACSL of the Frama-C software, dedicated to program verification at runtime.
I have a PhD in Computer Science from LIX, Ecole Polytechnique in the Cosynus team, under the supervision of Samuel Mimram and Eric Finster. My PhD thesis is mostly centered on the theorem prover for higher categories CaTT, and the theory behind it, relating to higher category theory and type theory.
My research interests are at the intersection between computer science and mathematics, and in particular in various aspects of computer languages: their semantics, their design and the verification of these languages.
Among computer languages, I am very interested in the flavours of type theories that I find very ubiquitous. I use a lot of of the interactive proof assisants based on them, and I like the connection they provide between programming, categorical logic and algebra.
I am also interested in higher dimensional algebra and the coherence problems that are at its core. This problem is ubiquitous and can be found in areas ranging from algebraic topology to the equality types of dependent type theory. I am very interested in homotopy type theory as a framework to unite these worlds and provide a connection between proofs, programs and spaces.
During my PhD, I have supervised the practicals Java beginner’s class at Ecole Polytechnique for three years, and for its follow-up class for two years. I have also done tutoring sessions in python and algorithmics for one year.