About me

I am an Engineer at Inria. I work on improving and promoting the Coq proof assistant, and on building a Consortium of academic and industrial users of Coq.

Coq

Coq is a fascinating piece of open-source software, that makes it possible to prove the correctness of programs or mechanically formalize the proof of mathematical theorems. Have a look at Coq’s website.

The Coq Consortium

A Consortium of academic and industrial users of Coq is being created by Inria. If you want to know more, don’t hesitate to contact me.