I have worked on the locally nameless approach to variable binding representation, which greatly helps in the formalization of programming language metatheory.
Intensive use of the Coq proof assistant has lead me to develop an extended set of tactics, as well as a practical approach to defining recursive functions.
I train the French team to the IOI, together with Mathias Hiron. We also try and promote the development of algorithmics in France among young students. Our website features on-line courses with computer-evaluated exercises. In French.
This course is designed for people who learn OCaml as a first programming language. It comes with a hundred interactive exercises that are integrated in the text. In French.
This website gathers high-quality teaching material for computer science courses preparing for research, both in french and english. I am the original designer and main administrator of this website; the current implementation is due to Guillaume Ryder.
