|
|
 |
|
Vendredi 17 Mars
| Heure: |
11:00 - 12:30 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Des preuves, oui, mais formelles ! |
| Description: |
Micaela MAYERO Dans cet exposé, très informel, lui, je parlerai de l'évolution des outils de preuves formelles ces 20, voire ces 30, dernières années. Nous nous appuierons sur quelques exemples afin de montrer comment les formalisations contribuent à la fois au développement de ces outils via des avancés théoriques majeurs ainsi qu'aux domaines qui s'engagent peu à peu dans leur utilisation. Suite à une première partie accessible à tout public, nous parlerons de la logique sous-jacente à l'un des système connaissant le plus d'avancées et de changements: Coq. Nous aborderons les évolutions de la théorie des types avec (im)prédicativité, la logique classique avec le choix de la totalité et d'autres avancées, pour finir, si nous avons le temps, par quelques mots sur CoqHoTT et l'axiome d'univalence. |
|
|
