I'm interested in using and teaching theoretical computer science and interactive theorem proving.

In 2004, Yves Bertot and me published the first book on Coq: "Interactive Theorem Proving and Program Development" (a.k.a. "Coq'Art") https://www-sop.inria.fr/lemme/Yves.Bertot/coqart.html .

I'm a member of https://github.com/coq-community, and developper of the https://github.com/coq-community/hydra-battles project (library and book about entertaining math in Coq).