Représentation des fonctions continues entre « streams » (& Co.) par des types de données
Pierre Hyvernat
LAMA, Université Savoie Mont Blanc
https://www.lama.univ-savoie.fr/pagesmembres/hyvernat/
Date(s) : 23/04/2015 iCal
11h00 - 12h00
Brouwer savait déjà que les fonctions continues entre streams (avec la topologie produit habituelle) pouvaient être représentées par des arbres infinis. Peter Hancock a montré comment interpréter ce théorème de représentation en théorie des types dépendants, permettant ainsi de manipuler ces fonctions comme un type de données (co)inductif standard.
Nous avons récemment pu généraliser ces idées à de nombreux types de données coinductifs en utilisant la notion de structure d’interaction (ou « container indexé » ou « foncteur polynomial »). Je présenterai cette généralisation en essayant d’introduire les notions nécessaires au fur et à mesure : topologie produit, types dépendants, définitions inductives et coinductives, systèmes d’interaction, définitions inductives-récursives, etc.
Travail en commun avec Peter Hancock.
http://www.lama.univ-savoie.fr/~hyvernat/
Catégories
