|
|
 |
|
Vendredi 30 Mars
| Heure: |
11:00 - 13:00 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Un calcul des séquents avec des types dépendants pour l'arithmétique classique |
| Description: |
Etienne MIQUEY En 2012, Hugo Herbelin définit dPA?, un langage typé qui fournit, dans un cadre compatible avec la logique classique, un terme de preuve pour laxiome du choix dépendant, qui peut être vu comme une adaptation de la preuve constructive de laxiome du choix en théorie des types de Martin-Löf ou une internalisation dans un système de preuve de lapproche en réalisabilité de Berardi, Bezem et Coquand. Malheureusement ce calcul ne dispose pas d'une preuve de normalisation, la difficulté d'une telle preuve est liée à la présence simultanée de types dépendants (pour la partie constructive du choix), d'opérateurs de contrôle (pour la logique classique), d'objets co-inductifs (pour "encoder" les fonctions de type N ? A par des streams (a?,a?,...)) et d'évaluation paresseuse avec partage (pour ces objets co-inductifs).
Durant cet exposé, nous verrons comment définir une variante de dPA? en calcul des séquents dont on pourra prouver la correction. Au passage, on montrera la normalisation du call-by-need classique (présenté comme une extension du ?µµ?-calcul avec des environnements partagés) en utilisant notamment des techniques de réalisabilité à la Krivine ; et l'on développera un calcul des séquents classique avec types dépendants, dont la correction est prouvable à l'aide d'une traduction CPS tenant compte des dépendances. |
|
|
