Intersection Types and Resource Calculi in the Denotational Semantics of λ-calculus – Federico Olimpieri

Federico Olimpieri
I2M, Aix-Marseille Université
/user/federico.olimpieri/

Date(s) : 27/11/2020   iCal
14 h 00 min - 16 h 00 min

Dirigée par Laurent Regnier, Lorenzo Tortora de Falco et Lionel Vaux Auclair et rapportée par Marcelo Fiore et Paul-André Melliès.

Manuscript: https://www.i2m.univ-amu.fr/perso/federico.olimpieri/these

La soutenance sera complètement dématérialisée, disponible à l’adresse :

https://greenlight.lal.cloud.math.cnrs.fr/b/lio-h2u-2ma

La presentation sera en anglais, devant le jury composé de:

– Marcelo Fiore (rapporteur), Cambridge University;

– Christine Tasson, Université Paris 6;

– Ugo dal Lago, Università degli studi di Bologna;

– Giuseppe Rosolini, Università di Genova;

– Lorenzo Tortora de Falco (directeur de thèse), Università degli studi Roma Tre;

– Laurent Regnier (directeur de thèse), Aix-Marseille Université;

– Lionel Vaux Auclair (directeur de thèse), Aix-Marseille Université.

Types intersection et calculs avec ressources dans la sémantique dénotationnelle du lambda-calcul.

Cette thèse étudie la notion d’approximation dans le lambda-calcul selon différentes perspectives. Ehrhard et Regnier ont introduit le développement de Taylor des lambda-termes: on peut voir un lambda-terme comme une série infinie des ses approximations linéaires. Une autre notion d’approximation dans le lambda-calcul est donné par les types intersection, introduits par Coppo et Dezani dans les années 80. Dans une première partie, nous étendons la définition standard du développement de Taylor à un lambda-calcul non-déterministe. On introduit un calcul avec ressources rigide et on établit une relation combinatoire entre les termes de ce calcul et les éléments du développement. On démontre un théorème de commutation entre développement de Taylor et arbres de Böhm dans ce contexte non-déterministe. Dans une deuxième partie de la thèse, on introduit le cadre bicatégorique des distributeurs. On présente une collection de 2-monades, les monades de ressources, et on les transpose dans la bicatégorie des distributeurs, en utilisant une méthode introduite par Fiore, Gambino, Hyland et Winskel. On considère les bicatégories de Kleisli pour ces pseudomonades et on donne une condition suffisante pour qu’une telle bicatégorie soit cartésienne fermée, donc un modèle du lambda-calcul simplement typé. Dans une troisième et dernière partie, on introduit les distributeurs de types intersections et, inspiré par le travail de Tsukada, Asada et Ong, le développement rigide des lambda-termes. Ces deux notions d’approximation sont une présentation syntaxique de la sémantique bicatégorique induite par les bicatégories de Kleisli étudiées dans la deuxième partie. La notion de distributeur de types intersections nous permet de considérer des systèmes de types intersections avec sous-typage. Ces modèles donnent une sémantique dénotationnelle sensible aux preuves, au sens où la sémantique d’un terme lui associe l’ensemble des ses dérivations de typage dans ces systèmes. Le sous-typage est induit par la structure particulière d’une catégorie de types. Notre construction est paramétrique sur les monades de ressources et produit quatre systèmes de types intersections. On montre que les distributeurs de types intersections sont naturellement isomorphes au développement rigide. On étudie ces structures sous réduction.

https://www.theses.fr/s189279

 

Catégories



Retour en haut 

Secured By miniOrange