I am currently a computer science professor in Classes préparatoires aux grandes écoles in Lycée Victor Hugo Besançon (french webpage).
Before this, I was a post-doctoral fellow at Inria Nancy - Grand Est, in the CAMUS team, located in Strasbourg. I was collaborating with Arthur Charguéraud to build an interface for source-to-source certified code transformations. Our main goal was in particular to use this interface for the optimisation of programs for PIC simulation.
In the past, I was a PhD student at Inria Sophia Antipolis - Méditerranée, in the MARELLE team. I was working under the supervision of Yves Bertot and Cyril Cohen. I studied the formalisation of classical analysis with the Coq proof assistant through a case study in control theory.
I am also a former civil servant student of the computer science department of the École Normale Supérieure de Lyon. For an overview of my education, have a look at my C.V. (in french).
My interests span all aspects of reasoning, especially with applications in mathematics and software verification. These include both theoretical and practical aspects of logic, foundations of mathematics, computer-aided reasoning, semantics…
My preferred medium for remote communication is e-mail. You may contact me at one of those addresses:
Current (temporary?) address (preferred by my current institute): firstname.lastname@example.org.
Permanent address (preferred by me): email@example.com.