During the first year of my master degree, I worked on a research project with the CIDRE team at INRIA under the direction of Emmanuelle Anceaume and Pierre Wilke. The goal was to prove, using the Coq proof assistant, some properties of Sycomore , a new blockchain desing. It was sadly cut short due to COVID19.
In 2020 and 2021, I did two internships with the CELTIQUE team at INRIA under the direction of Delphine Demange . I worked on the formalization and proof of compiler optimizations techniques based on monadic gated SSA (an intermediate representation based on dependency graphs rather than control-flow graphs).
Last updated on : 16 Dec 2021