I'm a PhD student at Laboratoire de Conception et d'Intégration des Systèmes (LCIS) (Lab for the Design and Integration of Systems) in Valence, France. I have the pleasure to work with Laure Gonnord and Christophe Deleuze. I got a theoretical background from my masters' at ENS de Lyon and now work to apply it on compilation and embedded software, where I have the most experience.
Here is a copy of my résumé.
Research projects #
In embedded systems
My Ph.D work focuses on getting counter-measures for fault injection and side-channels attacks up the compilation chain, by making the compiler generate fault-resistant code from source annotations.In formal verification
- Extensions of the congruence closure algorithm
Congruence closure is a standard algorithm for deciding equality — it essentially saturates a set of equalities using equivalence relation properties and the congruence rule
f = g -> x = y -> f x = g y. Interestingly, it can be generalized if we extend it to partial equivalence relations (PERs), leading to a more versatile semi-decision procedure. This work was supervised by Pierre Corbineau at Verimage (detailed report here). - Abstract semantics for monadic interpreters
An ongoing project with Yannick Zakowski. The Vellvm project has a fascinating semantic model for programs called Interaction Trees, which is a free monad (with non-termination). It makes it possible to define language semantics by starting with symbolic events for all non-trivial features (memory accesses, division, exceptions, etc.) then progressively refining the model by applying monad transformers onto the interaction tree, replacing each feature's symbolic events with their actual implementation.
I'm working on designing certified abstract interpreters using this progressive refinement model. The key is that it enables proving each feature's abstraction independently and then composing correctness proofs to prove the entire interpreter correct. This cuts down on the proof effort significantly. Challenges arise due to differences in control flow between the original program and its abstract version, which must be tracked. Paper on that coming soon, hopefully!
- Composable formal semantics for MLIR
On a trip to Tobias Grosser's team in Scotland I worked on prototyping formal semantics for MLIR, whose dialect-based extensibility is a very good match for Interaction Trees. This project was implemented in Lean 4, which has an incredibly satisfying meta-programming side. The Edinburgh team is working on polishing and publishing these results.
Teaching #
I work as a teaching assistant designing and supervising practicals at Grenoble INP - Ésisar, an engineering school with pretty wide coverage of automatics, electronics, and computer science. I've helped with the following classes:
- 2nd-year Algorithms and C programming;
- 2nd-year Recursive and functional programming (Haskell);
- 3rd-year Algorithms and C programming (up to a basic MIPS emulator).