My PhD thesis is mostly centered on the theorem prover for higher categories CaTT, and the theory behind it, relating to higher category theory and type theory.
My main interests revolve around higher dimensional algebra in general and everything related to the coherence problem that it spawns, from the mathematical point of view and from the computer science point of view. This ranges from homotopy theory and algebraic topology to type theory, and I am interested about homotopy type theory as a connection between these worlds. I work a lot with frameworks arising from categorical logic, and I would like to explore further the link with rewriting theory and higher dimensional versions of it.
During my PhD, I have supervised the practicals Java beginner’s class at Ecole Polytechnique for three years, and for its follow-up class for two years. I have also donce tutoring seesions in python and algorithmics for one year.