Related papers: Linear Rank Intersection Types
We characterize those intersection-type theories which yield complete intersection-type assignment systems for lambda-calculi, with respect to the three canonical set-theoretical semantics for intersection-types: the inference semantics,…
In this paper we define several notions of term expansion, used to define terms with less sharing, but with the same computational properties of terms typable in an intersection type system. Expansion relates terms typed by associative,…
We present a new approach to the following meta-problem: given a quantitative property of trees, design a type system such that the desired property for the tree generated by an infinitary ground $\lambda$-term corresponds to some property…
Multi types---aka non-idempotent intersection types---have been used to obtain quantitative bounds on higher-order programs, as pioneered by de Carvalho. Notably, they bound at the same time the number of evaluation steps and the size of…
We present a new type system combining refinement types and the expressiveness of intersection type discipline. The use of such features makes it possible to derive more precise types than in the original refinement system. We have been…
The intersection type assignment system has been designed directly as deductive system for assigning formulae of the implicative and conjunctive fragment of the intuitionistic logic to terms of lambda-calculus. But its relation with the…
Indexed Linear Logic has been introduced by Ehrhard and Bucciarelli, it can be seen as a logical presentation of non-idempotent intersection types extended through the relational semantics to the full linear logic. We introduce an…
The multiset based relational model of linear logic induces a semantics of the type free lambda-calculus, which corresponds to a non-idempotent intersection type system, System R. We prove that, in System R, the size of the type derivations…
We study an assignment system of intersection types for a lambda-calculus with records and a record-merge operator, where types are preserved both under subject reduction and expansion. The calculus is expressive enough to naturally…
One of the aims of Implicit Computational Complexity is the design of programming languages with bounded computational complexity; indeed, guaranteeing and certifying a limited resources usage is of central importance for various aspects of…
Type isomorphism is useful for retrieving library components, since a function in a library can have a type different from, but isomorphic to, the one expected by the user. Moreover type isomorphism gives for free the coercion required to…
We consider the call-by-value lambda-calculus extended with a may-convergent non-deterministic choice and a must-convergent parallel composition. Inspired by recent works on the relational semantics of linear logic and non-idempotent…
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…
We describe a type system with mixed linear and non-linear recursive types called LNL-FPC (the linear/non-linear fixpoint calculus). The type system supports linear typing, which enhances the safety properties of programs, but also supports…
We study the semantics of an untyped lambda-calculus equipped with operators representing read and write operations from and to a global store. We adopt the monadic approach to model side-effects and treat read and write as algebraic…
This article presents a novel approach to identifying and classifying intersections for semantic and topological mapping. More specifically, the proposed novel approach has the merit of generating a semantically meaningful map containing…
Evaluating higher-order functional programs through abstract machines inspired by the geometry of the interaction is known to induce $\textit{space}$ efficiencies, the price being $\textit{time}$ performances often poorer than those…
In this paper we invite the reader to a journey through three lambda calculi with resource control: the lambda calculus, the sequent lambda calculus, and the lambda calculus with explicit substitution. All three calculi enable explicit…
This paper investigates type isomorphism in a lambda-calculus with intersection and union types. It is known that in lambda-calculus, the isomorphism between two types is realised by a pair of terms inverse one each other. Notably,…
We define an equivalence relation on propositions and a proof system where equivalent propositions have the same proofs. The system obtained this way resembles several known non-deterministic and algebraic lambda-calculi.