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
George Manoussakis, lauréat 2018, prix de thèse (accessit) Charles Delorme
18 septembre 2018
George Manoussakis, est lauréat de prix de thèse (accessit) Ch. Delorme 2018. Il a soutenu sa thèse au LRI/Galac en Novembre 2017 sous la direction de J. Cohen et A. Deza. Depuis Septembre 2018 il est MdeC à l'Université de Versailles/Li-PaRAD.

TrackML dans Nature
21 janvier 2018
L'apprentissage automatique peut-il aider la physique des hautes énergies à découvrir et à caractériser de nouvelles particules ? TAO participe à l'organisation du challenge TrackML avec le CERN. La seconde phase de la compétition utilisera Codalab.

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