Intersection types and ressource calculi in the denotational semantics of lambda-calculus
Institution:
Aix-MarseilleDisciplines:
Directors:
Abstract EN:
This thesis studies the notion of approximation in lambda-calculus from different perspectives. In a first part, we extend the standard definition of Taylor expansion to a non-deterministic lambda-calculus. We introduce a rigid resource calculus and we establish a combinatorial relation between rigid resource terms and the elements of the Taylor expansion. We prove a commutation theorem between Taylor expansion and Böhm trees in this non-deterministic context.In a second part of the thesis, the bicategorical framework of distributors is introduced. We present a collection of doctrines, the resource monads, and we lift them to the bicategory of distributors, using a method introduced by Fiore, Gambino, Hyland and Winskel. We consider the Kleisli bicategories of these pseudomonads.In a third and last part, we introduce intersection type distributors and, inspired by 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 the semantics of a term associates to it the set of its typing derivations in appropriate systems. Our construction is parametric on resource monads and produces four intersection type systems. We show that intersection type distributors are naturally isomorphic to the rigid expansion. We study these structures under reduction.
Abstract FR:
Cette thèse étudie la notion d'approximation dans le lambda-calcul selon différentes perspectives. 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.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. On montre que les distributeurs de types intersections sont naturellement isomorphes au développement rigide. On étudie ces structures sous réduction.