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.