Français Anglais
Accueil Annuaire Plan du site
Accueil > News du laboratoire > Le logiciel Coq reçoit l'ACM SIGPLAN Software award
Le logiciel Coq reçoit l'ACM SIGPLAN Software award
Le logiciel Coq reçoit l'ACM SIGPLAN Software award Le logiciel Coq reçoit l'ACM SIGPLAN Software award
05 juillet 2003

L'assistant de preuve Coq, fruit d'un travail collectif débuté dans les années 80 et mené principalement à INRIA, ENS Lyon, Université Paris-Sud et Université Paris Diderot reçoit en 2013 le software award de l'ACM SIGPLAN.

L'assistant de preuve Coq propose un environnement sophistiqué pour le développement de preuves mathématiques vérifiées par ordinateur. La preuve du théorème des quatre couleurs, du théorème de Feit-Thomson (classification des groupes finis) ou encore le développement d'un compilateur C optimisant complètement prouvé sont des exemples emblématiques des possibilités de Coq. Le langage sous-jacent à cet outil (le calcul des constructions) a été proposé par Coquand et Huet en 84 puis étendu par Coquand et Paulin. Le système Coq a été développé activement depuis cette époque avec de nombreuses versions successives et la contribution de plus de 30 personnes. Le développement a été coordonné par Gérard Huet puis par Christine Paulin (de 1996 à 2002) et actuellement par Hugo Herbelin.



Pour en savoir plus: http://www.sigplan.org/Awards/Software/Main
News
Un article de Isabelle Guyon sur la démocratisation de l'IA
19 mars 2018
Lien vers l'article paru dans le journal le monde :
http://www.lemonde.fr/acces-restreint/sciences/article/2018/04/08/a4544bd07cad09fe52980c0f82c08b34_5282548_1650684.html

Michèle Sebag a été élue membre de l'Academie des Technologies
13 avril 2018
Michèle Sebag, DR CNRS et Directrice Adjointe du LRI, a été élue membre de l'Academie des Technologies

https://www.academie-technologies.fr/members/454-michele-sebag

Lin Chen a reçu la médaille de bronze du CNRS
27 mars 2018
Lin Chen, membre de l'équipe GALAC (https://www.lri.fr/~chen/) a reçu la médaille de bronze du CNRS. Ses principaux travaux de recherche portent sur la modélisation, l'analyse théorique, et la conception des algorithmes et protocoles distribués innovants