Coq’orico !

Des chercheurs français en informatique, dont Pierre Castéran maître de conférences au Labri, sont mis à l’honneur par un prestigieux prix international pour le développement d’un logiciel appelé Coq.

  • 29/04/2014

"Oiseau de feu"  © Michel Mendès France (université de Bordeaux) "Oiseau de feu" © Michel Mendès France (université de Bordeaux)

Dans un avion à 10 000 mètres d’altitude ou dans un train lancé à plus de 500 km/h, où les programmes informatiques sont légion, il suffirait d’un simple « bug » pour transformer un simple voyage en véritable catastrophe. Il est donc nécessaire que ces programmes aient été auparavant certifiés. Parmi les outils logiciels permettant de certifier les programmes figurent les « assistants à la preuve ». L’un d’entre eux Coq, développé par des chercheurs français depuis plus de 30 ans, reçoit aujourd’hui l’une des plus prestigieuses récompenses informatiques mondiales, le System Software Award 2013 de l’Association for computing machinery (ACM). Pierre Castéran, maître de conférences de l’université de Bordeaux, membre du Laboratoire bordelais de recherche en informatique (Labri), fait partie des neuf informaticiens mis à l’honneur par ce prix. Celui-ci récompense une institution ou des individus pour le développement d'un système logiciel particulièrement influent par sa contribution conceptuelle et/ou son acceptabilité commerciale. Pour n’en citer qu’un, en 1995, c’est le web ou plutôt le « world wide web » qui fut récompensé.

Cet ancien étudiant de l’université Paris Diderot, arrivé à Bordeaux en 1982, explique s’être tourné vers ce logiciel il y a une vingtaine d’années. « Je suis intéressé par les connexions entre mathématiques, informatique et logique, et c’est ce que je retrouvais au travers de Coq ». Pierre Castéran a d'abord été un utilisateur du système, bénéficiant des conseils de toute l'équipe de développement de Coq. De 2001 à 2004, il écrit avec Yves Bertot, du centre InriaInstitut national de recherche en informatique et en automatique de Sophia Antipolis, un livre destiné à être un ouvrage de référence à destination des chercheurs et doctorants, et un guide pour le rendre accessible.

Pierre Castéran et son livre Coq'art © Olivier Got

Enseigné dans des universités américaines

Les deux auteurs continuent à faire des mises à jour régulières de l'ouvrage en ligne afin de suivre la constante évolution du logiciel, et envisagent une nouvelle édition. Ce livre a beaucoup contribué à la diffusion de Coq sur tous les continents, et a même été traduit en mandarin. C'est à ce titre que Pierre Castéran figure dans la liste des récipiendaires, à côté des concepteurs et développeurs du logiciel. Il a également écrit des tutoriels avec d'autres développeurs de Coq, et participe à l'organisation d'écoles d'été en Chine, en France et au Japon.

Coq est un assistant de preuves qui intéresse les informaticiens mais aussi les mathématiciens. Il permet de faire des démonstrations très longues et compliquées de théorèmes mathématiques, comme par exemple le théorème dit des quatre couleurs ou plus récemment le théorème de Feit-Thompson. C'est un logiciel libre, aujourd'hui utilisé partout dans le monde. Il est enseigné dans les plus prestigieuses universités américaines et est le sujet de maintenant trois livres.

Ce prestigieux prix sera remis à l'équipe développant Coq le 21 juin prochain à San Francisco. Ce jour-là, c'est bien la recherche informatique française qui sera à l'honneur, une recherche sur le long terme, fruit de la collaboration de chercheurs de différents instituts, combinant mathématiques, informatique théorique et écriture de programmes complexes. C'est aussi l'alliance de la recherche et de la pédagogie qui est récompensée.

Références

Interactive Theorem Proving and Program Development
Coq’Art: The Calculus of Inductive Constructions
Series: Texts in Theoretical Computer Science. An EATCS Series
Bertot, Yves, Castéran, Pierre
2004, XXV, 472 p.

Oiseau de feu © Michel Mendès France

"Oiseau de feu" qui fait la couverture de l'ouvrage par Michel Mendès France (université de Bordeaux)

Thèmes :