• New draft available: "Abstract Interpreters: a Monadic Approach to Modular Verification". A work led by Sébastien Michelland! Joint work with Laure Gonnord and myself.
  • I joined the CoqPL'24 Program Comittee.
  • I joined the JFLA'24 Program Comittee.
  • Galaad Langlois has presented his work on formalizing W-types and M-types axiom free in Coq at the Coq Workshop 2023! Joint work with Damien Pous and myself.
  • Peio Borthelle has presented his ongoing talk on unifying and formalizing Operational Game Semantics at TYPES'23! Joint work with Guilhem Jaber, Tom Hirschowitz and myself.
  • I joined the POPL'24 Program Comittee.
  • Our paper "Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq" has been accepted for publication at POPL'23! Feel free to have a look at its repo as well!
  • Our paper "Formal Reasoning About Layered Monadic Interpreters" has been accepted for publication at ICFP'22! Catch Irene's talk at ICFP!
  • I will be part of the program commitee for ICFP'22!
  • I will be part of the program commitee for JFLA'21!
  • Check out our ICFP'21 paper describing the new semantics of Vellvm: Modular, Compositional, and Executable Formal Semantics for LLVM IR
  • About

    Since October 2020, I am a researcher 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 in here.

    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.