• I am delighted to have been admitted for an academic position at Inria! I will start on October 2020 in Lyon: beware of changes in virtual and physical addresses. Excited to start new collaborations!
  • I will be part of the program commitee for CPP'21!
  • About

    Starting from October 2020, I will be a research at Inria as a member of the CASH research group, hosted in the LIP research laboratory at ENS Lyon.

    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 notably work on the vellvm project, a formalization in the Coq proof assistant of LLVM's infrastructure, and LLVM IR's semantics in particular. 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 IR can be found here (draft).

    Before joining Inria, I was 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 still actively collaborate with Steve and other collaborators from Philadelphia, most notably as part of the Vellvm project.

    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 Lopez 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





    Current students





    Past research experiences

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