I am a postdoctoral researcher at the University of Pennsylvania, in the programming language research group, working with Steve Zdancewic as part of the DeepSpec NSF Expedition.

I am broadly interested in the formal verification of software, and have put so far through my work a particular emphasis on verified compilation. I formalize most of my work in the Coq proof assistant.

Currently, I mainly work on the vellvm project, a formalization in the Coq proof assistant of llvm's semantics. This led me to work on the representation of effectful programs in type theory, as well as new techniques to conduct coinductive reasoning. An account for the application of these techniques to model llvm is soon to come in "Modular Formal Semantics for the LLVM IR" (title subject to changes!).

Previously, I was a doctoral researcher in France in the Celtique team under the supervision of David Pichardie and David Cachera. I worked during this time on the formal verification of an on-the-fly concurrent garbage collector in the Coq proof assistant.

On a different note, I am extremely concerned by and interested in finding solutions for the need for all activities, and hence research in particular, to strive for carbon neutrality. I have worked with Crista Lopes and Benjamin Pierce as part of the SIGPLAN and climate change initiative. I have written a tool to estimate a conference's footprint and understand its source. I have co-authored a report (in progress) about the application of this tool to the major SIGPLAN conferences.

A curriculum vitae may be found here.


International Conferences






Teaching assistant during the three years of my PhD. I taught to various audiences, ranging from first year of bachelor to master students, both at the University of Rennes 1 and the ENS Rennes . I have notably been teaching assistant for the following courses:


Past research experiences

During my studies, I had the opportunities to do various internships in academia.