Café In le 17 janvier de 13h à 14h, Cafétaria, salle extension, présenté par Yves Bertot
En programmation, on utilise les types de données pour s’assurer que les programmes consomment toujours sur des données de bonne nature. L’idée de la théorie des types, c’est que la logique fonctionne pareil, les théorèmes sont des programmes et leurs hypothèses sont des données. Pour mettre cette idée en pratique, nous montrons deux approches: les tactiques et le mécanisme d’élaboration. Pour des travaux ambitieux, nous utilisons également un mécanisme de structuration et nous organisons les connaissances en bibliothèques.
Nous montrerons un exemple de calcul numérique dont la correction est vérifiée par ordinateur: les décimales de pi.
Les slides de la présentation.
13h : accueil avec café, thé
13h05-13h55 : présentation et discussion.
