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.