BEGIN:VCALENDAR VERSION:2.0 PRODID:-//wp-events-plugin.com//7.2.3.1//EN TZID:Europe/Paris X-WR-TIMEZONE:Europe/Paris BEGIN:VEVENT UID:6621@i2m.univ-amu.fr DTSTART;TZID=Europe/Paris:20201127T140000 DTEND;TZID=Europe/Paris:20201127T160000 DTSTAMP:20241209T192558Z URL:https://www.i2m.univ-amu.fr/evenements/intersection-types-and-resource -calculi-in-the-denotational-semantics-of-%ce%bb-calculus-federico-olimpie ri/ SUMMARY:Federico Olimpieri (I2M\, Aix-Marseille Université): Intersection Types and Resource Calculi in the Denotational Semantics of λ-calculus DESCRIPTION:Federico Olimpieri: Dirigée par Laurent Regnier\, Lorenzo Tort ora de Falco et Lionel Vaux Auclair et rapportée par Marcelo Fiore et Pau l-André Melliès.\n\nJury composé de:\n\n- Marcelo Fiore (rapporteur)\, Cambridge University\;\n- Christine Tasson\, Université Paris 6\;\n- Ugo dal Lago\, Università degli studi di Bologna\;\n- Giuseppe Rosolini\, Uni versità di Genova\;\n- Lorenzo Tortora de Falco (directeur de thèse)\, U niversità degli studi Roma Tre\;\n- Laurent Regnier (directeur de thèse) \, Aix-Marseille Université\;\n- Lionel Vaux Auclair (directeur de thèse )\, Aix-Marseille Université.\nTypes intersection et calculs avec ressour ces dans la sémantique dénotationnelle du lambda-calcul.\nCette thèse étudie la notion d'approximation dans le lambda-calcul selon différentes perspectives. Ehrhard et Regnier ont introduit le développement de Taylo r des lambda-termes: on peut voir un lambda-terme comme une série infinie des ses approximations linéaires. Une autre notion d’approximation dan s 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 éte ndons la définition standard du développement de Taylor à un lambda-cal cul 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 en tre développement de Taylor et arbres de Böhm dans ce contexte non-déte rministe. Dans une deuxième partie de la thèse\, on introduit le cadre b icaté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 p seudomonades et on donne une condition suffisante pour qu'une telle bicat égorie soit cartésienne fermée\, donc un modèle du lambda-calcul simpl ement typé. Dans une troisième et dernière partie\, on introduit les di stributeurs de types intersections et\, inspiré par le travail de Tsukada \, Asada et Ong\, le développement rigide des lambda-termes. Ces deux not ions d’approximation sont une présentation syntaxique de la sémantique bicatégorique induite par les bicatégories de Kleisli étudiées dans l a deuxième partie. La notion de distributeur de types intersections nous permet de considérer des systèmes de types intersections avec sous-typag e. Ces modèles donnent une sémantique dénotationnelle sensible aux preu ves\, 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 construc tion est paramétrique sur les monades de ressources et produit quatre sys tèmes de types intersections. On montre que les distributeurs de types in tersections sont naturellement isomorphes au développement rigide. On ét udie ces structures sous réduction.\nIntersection Types and Resource Calc uli in the Denotational Semantics of λ-calculus.\nThis thesis studies the notion of approximation in the lambda-calculus from different perspective s. Ehrhard and Regnier introduced the Taylor expansion of lambda-terms: we can see a lambda-term as an infinite series of its linear approximations. Another notion of approximation in the lambda-calculus is given by the in tersection types\, introduced by Coppo and Dezani in the 1980s. In the fir st part\, we extend the standard definition of Taylor's expansion to a non -deterministic lambda-calculus . One introduces a calculation with rigid r esources and one establishes a combinatorial relation between the terms of this calculation and the elements of the development. We prove a switchin g theorem between Taylor expansion and Böhm trees in this non-determinist ic context. In a second part of the thesis\, we introduce the bicategoric framework of distributors. We present a collection of 2-monads\, the resou rce monads\, and transpose them into the bicategory of distributors\, usin g a method introduced by Fiore\, Gambino\, Hyland and Winskel. We consider the Kleisli bicategories for these pseudomonads and we give a sufficient condition for such a bicategory to be closed Cartesian\, hence a simply ty ped model of the lambda-calculus. In a third and final part\, we introduce intersection type distributors and\, inspired by the work of Tsukada\, As ada and Ong\, the rigid development of lambda-terms. These two notions of approximation are a syntactic presentation of the bicategoric semantics in duced by the Kleisli bicategories studied in the second part. The notion o f intersection type distributor allows us to consider intersection type sy stems with subtyping. These models provide proof-sensitive denotational se mantics\, in the sense that the semantics of a term associate with it all of its typing derivations in these systems. Subtyping is induced by the pa rticular structure of a category of types. Our construction is parametric on resource monads and produces four systems of intersection types. We sho w that intersection-type distributors are naturally isomorphic with rigid development. We study these structures under reduction.\nLien : https://th eses.fr/2020AIXM0380 ATTACH;FMTTYPE=image/jpeg:https://www.i2m.univ-amu.fr/wp-content/uploads/2 020/11/Federico_Olimpieri.jpg CATEGORIES:Soutenance de thèse,AGLR,Logique et Interactions END:VEVENT BEGIN:VTIMEZONE TZID:Europe/Paris X-LIC-LOCATION:Europe/Paris BEGIN:STANDARD DTSTART:20201025T020000 TZOFFSETFROM:+0200 TZOFFSETTO:+0100 TZNAME:CET END:STANDARD END:VTIMEZONE END:VCALENDAR