Pierre HYVERNAT – Représentation des fonctions continues entre « streams » (& Co.) par des types de données

Carte non disponible
Speaker Home page :
Speaker :
Speaker Affiliation :

()

Date/heure
Date(s) - 23/04/2015
11 h 00 min - 12 h 00 min

Catégories


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/« >http://www.lama.univ-savoie.fr/~hyvernat/


Retour en haut 

Secured By miniOrange