Professional activities
I am currently working within the TypiCal project. I am involved in the development of the Coq proof assistant, under the supervision of Benjamin Werner. I am currently implementing a framework for specifying languages with binders within Coq. We intend to use higher-order abstract syntax as a user-interface, and normalization by evaluation as a backend for the system.
Occasionally, I participate in teaching activities at École Polytechnique, within the Principles of Programming Languages module.