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

Autor: Olimpieri, Federico
Přispěvatelé: Institut de Mathématiques de Marseille (I2M), Aix Marseille Université (AMU)-École Centrale de Marseille (ECM)-Centre National de la Recherche Scientifique (CNRS), Aix-Marseille Université, L. Regnier, L. Vaux Auclair, L. Tortora de Falco
Jazyk: angličtina
Rok vydání: 2020
Předmět:
Zdroj: Mathematics [math]. Aix-Marseille Université, 2020. English. ⟨NNT : ⟩
Popis: This thesis studies the notion of approximation in lambda-calculus from differentperspectives.Ehrhard and Regnier introduced the Taylor expansion of lambda-terms: onecan see a lambda-term as an infinite formal sum of its linear approximants. Another notion of approximation in lambda-calculus is given by intersection types,introduced by Coppo and Dezani in the 80s.In a first part, we extend the standard definition of Taylor expansion to anon-deterministic lambda-calculus. We introduce a rigid resource calculus and weestablish a combinatorial relation between rigid resource terms and the elements ofthe Taylor expansion. We prove a commutation theorem between Taylor expansionand Böhm trees in this non-deterministic context.In a second part of the thesis, the bicategorical framework of distributors isintroduced. We present a collection of doctrines, the resource monads, and welift them to the bicategory of distributors, using a method introduced by Fiore,Gambino, Hyland and Winskel. We consider the Kleisli bicategories of thesepseudomonads and we give a sufficient condition that makes these bicategoriescartesian closed, thus models of simply typed lambda-calculus.In a third and last part, we introduce intersection type distributors and, inspiredby the work of Tsukada, Asada and Ong, the rigid expansion of lambda-terms.These two notions of approximation are a syntactic presentation of the bicategorical semantics induced by the Kleisli constructions studied in the second part.Intersection type distributors determine intersection type systems with subtyping.This model gives a proof-relevant denotational semantics, in the sense that thesemantics of a term associates to it the set of its typing derivations in appropriatesystems. Subtyping is induced from the particular structure of a category of types.Our construction is parametric on resource monads and produces four intersectiontype systems. We show that intersection type distributors are naturally isomorphicto the rigid expansion. We study these structures under reduction.; 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 approximationslinéaires. Une autre notion d’approximation dans le lambda-calcul est donné parles types intersections, 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 avecressources rigide et on établit une relation combinatoire entre les termes de ce calculet les éléments du développement. On démontre un théorème de commutation entredé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 desdistributeurs. 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éthodeintroduite par Fiore, Gambino, Hyland et Winskel. On considère les bicatégoriesde Kleisli pour ces pseudomonades et on donne une condition suffisante pourqu’une telle bicatégorie soit cartésienne fermée, donc un modèle du lambda-calculsimplement typé.Dans une troisième et dernière partie, on introduit les distributeurs de typesintersections et, inspiré par le travail de Tsukada, Asada et Ong, le développementrigide des lambda-termes. Ces deux notions d’approximation sont une présentationsyntaxique 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 intersectionsnous permet de considérer des systèmes de types intersections avec sous-typage. Cesmodè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 dansces systèmes. Le sous-typage est induit par la structure particulière d’une catégoriede types. Notre construction est paramétrique sur les monades de ressources etproduit quatre systèmes de types intersections. On montre que les distributeursde types intersections sont naturellement isomorphes au développement rigide. Onétudie ces structures sous réduction.
Databáze: OpenAIRE
Externí odkaz: