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
Prix de stage de recherche de l'École polytechnique
19 novembre 2019
Quentin Soubeyran a reçu le prix de stage de recherche de l'École polytechnique pour son travail au LRI dans l'équipe Systèmes Parallèles.

Prix FIEEC CARNOT de la recherche appliquée
18 octobre 2019
Claude Marché remporte le premier prix FIEEC CARNOT de la recherche appliquée pour sa collaboration avec la société AdaCore.

Ouvrage Informatique au lycée
24 septembre 2019
Parution d'un ouvrage pour la spécialité NSI en classe de première, co-écrit par quatre membres du LRI.