Search

This artifact contains the mechanical formalization of the calculi associated with the paper Dependent Merges and First-Class Environments. All of the metatheory has been formalized in Coq theorem prover. The paper studies a statically typed calculus, called 𝖤_i, with first-class environments. The main novelty of the 𝖤_i calculus is its support for first-class environments, together with an expressive set of operators that manipulate them., DARTS, Vol. 9, Special Issue of the 37th European Conference on Object-Oriented Programming (ECOOP 2023), pages 2:1-2:3

In most programming languages a (runtime) environment stores all the definitions that are available to programmers. Typically, environments are a meta-level notion, used only conceptually or internally in the implementation of programming languages. Only a few programming languages allow environments to be first-class values, which can be manipulated directly in programs. Although there is some research on calculi with first-class environments for statically typed programming languages, these calculi typically have significant restrictions. In this paper we propose a statically typed calculus, called 𝖤_i, with first-class environments. The main novelty of the 𝖤_i calculus is its support for first-class environments, together with an expressive set of operators that manipulate them. Such operators include: reification of the current environment, environment concatenation, environment restriction, and reflection mechanisms for running computations under a given environment. In 𝖤_i any type can act as a context (i.e. an environment type) and contexts are simply types. Furthermore, because 𝖤_i supports subtyping, there is a natural notion of context subtyping. There are two important ideas in 𝖤_i that generalize and are inspired by existing notions in the literature. The 𝖤_i calculus borrows disjoint intersection types and a merge operator, used in 𝖤_i to model contexts and environments, from the λ_i calculus. However, unlike the merges in λ_i, the merges in 𝖤_i can depend on previous components of a merge. From implicit calculi, the 𝖤_i calculus borrows the notion of a query, which allows type-based lookups on environments. In particular, queries are key to the ability of 𝖤_i to reify the current environment, or some parts of it. We prove the determinism and type soundness of 𝖤_i, and show that 𝖤_i can encode all well-typed λ_i programs., LIPIcs, Vol. 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023), pages 34:1-34:32

International audience; We show that an intuitionistic version of counting propositional logic corresponds, in the sense of Curry and Howard, to an expressive type system for the probabilistic event λ-calculus, a vehicle calculus in which both call-by-name and call-by-value evaluation of discrete randomized functional programs can be simulated. In this context, proofs (respectively, types) do not guarantee that validity (respectively, termination) holds, but reveal the underlying probability. We finally show how to obtain a system precisely capturing the probabilistic behavior of λ-terms, by endowing the type system with an intersection operator.

The recently proposed CP language adopts Compositional Programming: a new modular programming style that solves challenging problems such as the Expression Problem. CP is implemented on top of a polymorphic core language with disjoint intersection types called 𝖥_{i}^{+}. The semantics of 𝖥_{i}^{+} employs an elaboration to a target language and relies on a sophisticated proof technique to prove the coherence of the elaboration. Unfortunately, the proof technique is technically challenging and hard to scale to many common features, including recursion or impredicative polymorphism. Thus, the original formulation of 𝖥_{i}^{+} does not support the two later features, which creates a gap between theory and practice, since CP fundamentally relies on them. This paper presents a new formulation of 𝖥_{i}^{+} based on a type-directed operational semantics (TDOS). The TDOS approach was recently proposed to model the semantics of languages with disjoint intersection types (but without polymorphism). Our work shows that the TDOS approach can be extended to languages with disjoint polymorphism and model the full 𝖥_{i}^{+} calculus. Unlike the elaboration semantics, which gives the semantics to 𝖥_{i}^{+} indirectly via a target language, the TDOS approach gives a semantics to 𝖥_{i}^{+} directly. With a TDOS, there is no need for a coherence proof. Instead, we can simply prove that the semantics is deterministic. The proof of determinism only uses simple reasoning techniques, such as straightforward induction, and is able to handle problematic features such as recursion and impredicative polymorphism. This removes the gap between theory and practice and validates the original proofs of correctness for CP. We formalized the TDOS variant of the 𝖥_{i}^{+} calculus and all its proofs in the Coq proof assistant., LIPIcs, Vol. 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022), pages 18:1-18:28

We extend classic union and intersection type systems with a type-case construction and show that the combination of the union elimination rule of the former and the typing rules for type-cases of our extension encompasses occurrence typing . To apply this system in practice, we define a canonical form for the expressions of our extension, called MSC-form. We show that an expression of the extension is typable if and only if its MSC-form is, and reduce the problem of typing the latter to the one of reconstructing annotations for that term. We provide a sound algorithm that performs this reconstruction and a proof-of-concept implementation.

This artifact contains the mechanical formalization of the calculi associated with the paper Union Types with Disjoint Switches. All of the metatheory has been formalized in Coq theorem prover. We provide a docker image as well the code archive. The paper studies a union calculus ({λ_{u}}). Primary idea of {λ_{u}} calculus is a type based disjoint switch construct for the elimination of union types. We also study several extensions of the {λ_{u}} calculus including intersection types, distributive subtyping, nominal types, parametric polymorphism and an extension for the empty types., DARTS, Vol. 8, Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022), pages 17:1-17:6

Our companion paper proposes a new formulation of the 𝖥_{i}^{+} calculus with disjoint polymorphism and a merge operator based on Type-Directed Operational Semantics. The artifact contains Coq formalization of the 𝖥_{i}^{+} calculus and our new implementation of the CP language, which demonstrates the new 𝖥_{i}^{+} can serve as the direct foundation for Compositional Programming., DARTS, Vol. 8, Special Issue of the 36th European Conference on Object-Oriented Programming (ECOOP 2022), pages 4:1-4:3

Union types are nowadays a common feature in many modern programming languages. This paper investigates a formulation of union types with an elimination construct that enables case analysis (or switches) on types. The interesting aspect of this construct is that each clause must operate on disjoint types. By using disjoint switches, it is possible to ensure exhaustiveness (i.e. all possible cases are handled), and that none of the cases overlap. In turn, this means that the order of the cases does not matter and that reordering the cases has no impact on the semantics, helping with program understanding and refactoring. While implemented in the Ceylon language, disjoint switches have not been formally studied in the research literature, although a related notion of disjointness has been studied in the context of disjoint intersection types. We study union types with disjoint switches formally and in a language independent way. We first present a simplified calculus, called the union calculus (λ_u), which includes disjoint switches and prove several results, including type soundness and determinism. The notion of disjointness in λ_u is in essence the dual notion of disjointness for intersection types. We then present a more feature-rich formulation of λ_u, which includes intersection types, distributive subtyping and a simple form of nominal types. This extension reveals new challenges. Those challenges require us to depart from the dual notion of disjointness for intersection types, and use a more general formulation of disjointness instead. Among other applications, we show that disjoint switches provide an alternative to certain forms of overloading, and that they enable a simple approach to nullable (or optional) types. All the results about λ_u and its extensions have been formalized in the Coq theorem prover., LIPIcs, Vol. 222, 36th European Conference on Object-Oriented Programming (ECOOP 2022), pages 25:1-25:31

We study encodings of the λ-calculus into the π-calculus in the unexplored case of calculi with non-determinism and failures. On the sequential side, we consider λ^↯_⊕, a new non-deterministic calculus in which intersection types control resources (terms); on the concurrent side, we consider 𝗌π, a π-calculus in which non-determinism and failure rest upon a Curry-Howard correspondence between linear logic and session types. We present a typed encoding of λ^↯_⊕ into 𝗌π and establish its correctness. Our encoding precisely explains the interplay of non-deterministic and fail-prone evaluation in λ^↯_⊕ via typed processes in 𝗌π. In particular, it shows how failures in sequential evaluation (absence/excess of resources) can be neatly codified as interaction protocols., LIPIcs, Vol. 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), pages 21:1-21:22

Type-preserving translations are effective rigorous tools in the study of core programming calculi. In this paper, we develop a new typed translation that connects sequential and concurrent calculi; it is governed by type systems that control resource consumption. Our main contribution is the source language, a new resource λ-calculus with non-collapsing non-determinism and failures, dubbed uλ^{↯}_{⊕}. In uλ^{↯}_{⊕}, resources are split into linear and unrestricted; failures are explicit and arise from this distinction. We define a type system based on intersection types to control resources and fail-prone computation. The target language is 𝗌π, an existing session-typed π-calculus that results from a Curry-Howard correspondence between linear logic and session types. Our typed translation subsumes our prior work; interestingly, it treats unrestricted resources in uλ^{↯}_{⊕} as client-server session behaviours in 𝗌π., LIPIcs, Vol. 239, 27th International Conference on Types for Proofs and Programs (TYPES 2021), pages 11:1-11:24

We investigate intersection types and resource lambda-calculus in deep-inference proof theory. We give a unified type system that is parametric in various aspects: it encompasses resource calculi, intersection-typed lambda-calculus, and simply-typed lambda-calculus; it accommodates both idempotence and non-idempotence; it characterizes strong and weak normalization; and it does so while allowing a range of algebraic laws to determine reduction behaviour, for various quantitative effects. We give a parametric resource calculus with explicit sharing, the "collection calculus", as a Curry-Howard interpretation of the type system, that embodies these computational properties., LIPIcs, Vol. 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), pages 24:1-24:24

The quest for a fully abstract model of the call-by-value λ-calculus remains crucial in programming language theory, and constitutes an ongoing line of research. While a model enjoying this property has not been found yet, this interesting problem acts as a powerful motivation for investigating classes of models, studying the associated theories and capturing operational properties semantically. We study a relational model presented as a relevant intersection type system, where intersection is in general non-idempotent, except for an idempotent element that is injected in the system. This model is adequate, equates many λ-terms that are indeed equivalent in the maximal observational theory, and satisfies an Approximation Theorem w.r.t. a system of approximants representing finite pieces of call-by-value Böhm trees. We show that these tools can be used for characterizing the most significant properties of the calculus - namely valuability, potential valuability and solvability - both semantically, through the notion of approximants, and logically, by means of the type assignment system. We mainly focus on the characterizations of solvability, as they constitute an original result. Finally, we prove the decidability of the inhabitation problem for our type system by exhibiting a non-deterministic algorithm, which is proven sound, correct and terminating., LIPIcs, Vol. 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021), pages 7:1-7:18

A representation of intersection types in terms of pregrammars is presented. Pregrammar based rewriting relations, corresponding respectively to type checking and inhabitation are defined and the latter is used to implement a Wajsberg/Ben-Yelles style alternating semi-decision algorithm for inhabitation. The usefulness of the framework is illustrated by revisiting and partially extending standard inhabitation related results for intersection types, as well as establishing new ones. It is shown how the notion of bounded multiset dimension emerges naturally and the relation between the two settings is clarified. A meaningful rank independent superset of the set of rank 2 types is identified for which EXPSPACE-completeness for inhabitation as well as for counting is proved. Finally, a standard result on negatively non-duplicated simple types is extended to intersection types., LIPIcs, Vol. 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), pages 14:1-14:22

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.

International audience; The notion of solvability, crucial in the λ-calculus, is conservatively extended to a probabilistic setting, and a complete characterization of it is given. The employed technical tool is a type assignment system, based on non-idempotent intersection types, whose typable terms turn out to be precisely the terms which are solvable with nonnull probability. We also supply an operational characterization of solvable terms, through the notion of head normal form, and a denotational model of Λ⊕, itself induced by the type system, which equates all the unsolvable terms.

International audience; Twenty years ago, in an article titled "Covariance and contravariance: conflict without a cause", I argued that covariant and contravariant specialization of method parameters in object-oriented programming had different purposes and deduced that, not only they could, but actually they should both coexist in the same language. In this work I reexamine the result of that article in the light of recent advances in (sub-)typing theory and programming languages, taking a fresh look at this old issue. Actually, the revamping of this problem is just an excuse for writing an essay that aims at explaining sophisticated type-theoretic concepts, in simple terms and by examples, to undergraduate computer science students and/or willing functional programmers. Finally, I took advantage of this opportunity to describe some undocumented advanced techniques of type-systems implementation that are known only to few insiders that dug in the code of some compilers: therefore, even expert language designers and implementers may find this work worth of reading.

Calculi with disjoint intersection types and a merge operator provide general mechanisms that can subsume various other features. Such calculi can also encode highly dynamic forms of object composition, which capture common programming patterns in dynamically typed languages (such as JavaScript) in a fully statically typed manner. Unfortunately, unlike many other foundational calculi (such as System F, System F_{< :} or Featherweight Java), recent calculi with the merge operator lack a (direct) operational semantics with standard and expected properties such as determinism and subject-reduction. Furthermore the metatheory for such calculi can only account for terminating programs, which is a significant restriction in practice. This paper proposes a type-directed operational semantics (TDOS) for λ_i^{:}: a calculus with intersection types and a merge operator. The calculus is inspired by two closely related calculi by Dunfield (2014) and Oliveira et al. (2016). Although Dunfield proposes a direct small-step semantics for her calculus, her semantics lacks both determinism and subject-reduction. Using our TDOS we obtain a direct semantics for λ_i^{:} that has both properties. To fully obtain determinism, the λ_i^{:} calculus employs a disjointness restriction proposed in Oliveira et al.’s λ_i calculus. As an added benefit the TDOS approach deals with recursion in a straightforward way, unlike λ_i and subsequent calculi where recursion is problematic. To further relate λ_i^{:} to the calculi by Dunfield and Oliveira et al. we show two results. Firstly, the semantics of λ_i^{:} is sound with respect to Dunfield’s small-step semantics. Secondly, we show that the type system of λ_i^{:} is complete with respect to the λ_i type system. All results have been fully formalized in the Coq theorem prover., LIPIcs, Vol. 166, 34th European Conference on Object-Oriented Programming (ECOOP 2020), pages 26:1-26:32

We present the syntax, semantics, typing, subtyping, unification, refinement, and REPL of BULL, a prototype theorem prover based on the Δ-Framework, i.e. a fully-typed Logical Framework à la Edinburgh LF decorated with union and intersection types, as described in previous papers by the authors. BULL also implements a subtyping algorithm for the Type Theory Ξ of Barbanera-Dezani-de'Liguoro. BULL has a command-line interface where the user can declare axioms, terms, and perform computations and some basic terminal-style features like error pretty-printing, subexpressions highlighting, and file loading. Moreover, it can typecheck a proof or normalize it. These terms can be incomplete, therefore the typechecking algorithm uses unification to try to construct the missing subterms. BULL uses the syntax of Berardi’s Pure Type Systems to improve the compactness and the modularity of the kernel. Abstract and concrete syntax are mostly aligned and similar to the concrete syntax of Coq. BULL uses a higher-order unification algorithm for terms, while typechecking and partial type inference are done by a bidirectional refinement algorithm, similar to the one found in Matita and Beluga. The refinement can be split into two parts: the essence refinement and the typing refinement. Binders are implemented using commonly-used de Bruijn indices. We have defined a concrete language syntax that will allow user to write Δ-terms. We have defined the reduction rules and an evaluator. We have implemented from scratch a refiner which does partial typechecking and type reconstruction. We have experimented BULL with classical examples of the intersection and union literature, such as the ones formalized by Pfenning with his Refinement Types in LF and by Pierce. We hope that this research vein could be useful to experiment, in a proof theoretical setting, forms of polymorphism alternatives to Girard’s parametric one.

This paper shows that the recent approach to quantitative typing systems for programming languages can be extended to pattern matching features. Indeed, we define two resource-aware type systems, named U and E, for a λ-calculus equipped with pairs for both patterns and terms. Our typing systems borrow some basic ideas from [Antonio Bucciarelli et al., 2015], which characterises (head) normalisation in a qualitative way, in the sense that typability and normalisation coincide. But, in contrast to [Antonio Bucciarelli et al., 2015], our systems also provide quantitative information about the dynamics of the calculus. Indeed, system U provides upper bounds for the length of (head) normalisation sequences plus the size of their corresponding normal forms, while system E, which can be seen as a refinement of system U, produces exact bounds for each of them. This is achieved by means of a non-idempotent intersection type system equipped with different technical tools. First of all, we use product types to type pairs instead of the disjoint unions in [Antonio Bucciarelli et al., 2015], which turn out to be an essential quantitative tool because they remove the confusion between "being a pair" and "being duplicable". Secondly, typing sequents in system E are decorated with tuples of integers, which provide quantitative information about normalisation sequences, notably time (cf. length) and space (cf. size). Moreover, the time resource information is remarkably refined, because it discriminates between different kinds of reduction steps performed during evaluation, so that beta, substitution and matching steps are counted separately. Another key tool of system E is that the type system distinguishes between consuming (contributing to time) and persistent (contributing to space) constructors.

Our companion paper proposes a type-directed operational semantics (TDOS) for λ_i^{:}: a calculus with intersection types and a merge operator. The artifact contains the specification of λ_i^{:} and its TDOS, and related Coq code. λ_i^{:} is formalized using the locally nameless representation with cofinite quantification. The Coq definition and some infrastructure code are generated by Ott and LNgen. λ_i^{:} is inspired by two closely related calculi by Dunfield (2014) and Oliveira et al. (2016), and a simple variant of it is designed to demonstrate the possibility to match with them without any modification. To relate the two calculi with λ_i^{:}, a sound theorem on semantics and a completeness theorem on typing are proved for each variant. In addition, we extended the bidirectional typing of Oliveira et al.’s λ_i calculus, and designed an elaboration from it to λ_i^{:}, to show that many of λ_i^{:}’s explicit annotations can be inferred automatically., DARTS, Vol. 6, Special Issue of the 34th European Conference on Object-Oriented Programming (ECOOP 2020), pages 9:1-9:4

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.