Sites Inria

Événement

Cours de Gérard Berry et séminaire

Gérard Berry, titulaire de la Chaire "Algorithmes, Machines et langages" du Collège de France, donnera son premier cours de l'année 2018-2019 intitulé "Où va l'informatique ?" à Bordeaux,  sur le campus universitaire de Talence, le jeudi 13 décembre à 16h.

  • Date : 13/12/2018
  • Lieu : Agora du Haut-Carré - 43 rue Pierre Noailles - 33405 Talence

Cours de Gérard Berry

Où va l'informatique ?

"En théorie, la théorie et la pratique c'est pareil, en pratique c'est pas vrai."

Cette fameuse maxime de Yogi Berra, grand joueur de baseball et grand créateur d’aphorismes, s’applique parfaitement à la recherche en informatique.
L’exposé discutera quatre types de cas à travers des exemples variés.
D’abord, les cas où la théorie est claire mais la pratique de tous les jours confuse. C’est le cas des probabilités, très contre-intuitives, où nous analysons en particulier les étranges réactions aux jeux de type Loto et "Monty Hall Problem", qui a défrayé la chronique dans les années quatre-vingt-dix.
Ensuite, les cas où la théorie est peu opérante mais la pratique étonnamment efficace, à travers en particulier le calcul Booléen, problème NP-complet typique qu’on ne pensait pas soluble en pratique mais qu’on résout pourtant étonnamment bien dans des cas réels de grande taille - sans d’ailleurs qu’on sache vraiment pourquoi.

Nous parlerons aussi des fausses croyances pseudo-théoriques très répandues mais battues en brèche par la pratique, comme celle de la fin de la Loi de Moore pour les circuits ou celle de la puissance infinie des ordinateurs quantiques.

Nous verrons ensuite un cas où la théorie et la pratique coopèrent ou rentrent en conflit alternativement au cours du temps, celui de l’évolution de la programmation et de ses langages.

Nous terminerons par les cas où la théorie et la pratique sont quasiment fusionnelles, par exemple en algorithmique randomisée moderne, en vérification formelle de programmes et théorèmes, ou en simulation des phénomènes physiques et biologiques. 

  • 16h-17h30 à l'Agora du Haut-Carré 

Séminaire suivant le cours

Coq : aspects pratiques de la théorie des types

Yves Bertot - Inria Sophia-Antipolis et Pierre Castéran - Labri, Laboratoire Bordelais de Recherche en Informatique

Les assistants de preuve ont deux types d’applications : la construction de preuves formelles de correction de programmes ou d'algorithmes très complexes (compilateurs et analyseurs statiques, algorithmes distribués, protocoles cryptographiques, etc. ), et celle de preuves formelles de théorèmes requérant l'étude de nombreux cas complexes (théorèmes des quatre couleurs, théorème de Feit-Thompson sur la classification des groupes, conjecture de Kepler sur le rangement optimal des sphère, etc.). Ces preuves sont en général très volumineuses, ce qui pose deux problèmes majeurs. D’abord, aucun être humain ne peut en écrire tous les détails ; ceux-ci sont créés en machine suivant les stratégies et indications fines fournies par l'utilisateur ou utilisatrice.

Ensuite, la confiance en la correction d’une preuve écrite à l'aide d'un assistant de preuve provient de celle qu'on accorde au programme de vérification de preuves présent dans le noyau de cet assistant. 

À l'aide de quelques exemples, nous abordons les questions suivantes : 

  • Comment diriger un assistant de preuves de façon à vérifier un programme ou un théorème mathématique ? 
  • Comment convaincre une tierce personne qu'un long développement en Coq prouve bien le résultat annoncé ? 

La réponse à ces questions tient en deux aspects : d'un point de vue pratique, développer des « patrons de preuve » similaires aux « patrons de conception » de la programmation ; comprendre la logique mathématique utilisée par l'assistant de preuve et valider la correction de l'algorithme de vérification des preuves. 

  • 17h30-18h30 à l'Agora du Haut-Carré 

Informations pratiques

GERARD BERRY

Ancien élève de l’École polytechnique, ingénieur général du Corps des mines, membre de l’Académie des sciences, de l’Académie des technologies et de l’Academia Europaea , Gérard Berry a été chercheur à l’École des mines de Paris et à l'Inria de 1970 à 2000, Directeur scientifique de la société Esterel Technologies de 2001 à 2009 puis Directeur scientifique Inria et président de la Commission d’évaluation de cet institut de 2009 à 2012. Il tient la chaire "Informatique et sciences numériques" au Collège de France depuis 2012, après y avoir tenu deux chaires annuelles en 2007-2008 et 2009-2010.


Sa contribution scientifique concerne quatre sujets principaux :

  • le traitement formel des langages de programmation et leurs relations avec la logique mathématique,
  • la programmation parallèle et temps réel,
  • la conception assistée par ordinateur de circuits intégrés,
  • la vérification formelle des programmes et circuits.

Il est le créateur du langage de programmation Esterel .

Haut de page

Suivez Inria