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
Motion du LRI contre la LPPR
26 juin 2020

Ouvrage Informatique au lycée
18 juin 2020
Parution d'un ouvrage pour la spécialité NSI en classe de terminale, co-écrit par quatre membres du LRI.

Eugénie Brasier - 2ème prix MT180 PSaclay
07 avril 2020
Eugénie Brasier a eu le 2ème prix de Ma Thèse en 180 secondes de Paris-Saclay.