Séminaire Marelle : Automatisation de preuves en Coq par traduction en logique du premier ordre
Coq, les maths ont trouvé leur maître (Article de Science et Vie magazine)
Jul 29 2013
http://hal.inria.fr/hal-00816699/en/