ﻻ يوجد ملخص باللغة العربية
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, invertible terms are linear terms of a particular shape, called finite hereditary permutators. Typing properties of finite hereditary permutators are then studied in a relevant type inference system with intersection and union types for linear terms. In particular, an isomorphism preserving reduction between types is defined. Type reduction is confluent and terminating, and induces a notion of normal form of types. The properties of normal types are a crucial step toward the complete characterisation of type isomorphism. The main results of this paper are, on one hand, the fact that two types with the same normal form are isomorphic, on the other hand, the characterisation of the isomorphism between types in normal form, modulo isomorphism of arrow types.
Non-idempotent intersection types are used in order to give a bound of the length of the normalization beta-reduction sequence of a lambda term: namely, the bound is expressed as a function of the size of the term.
In this paper we investigate the $lambda$ -calculus, a $lambda$-calculus enriched with resource control. Explicit control of resources is enabled by the presence of erasure and duplication operators, which correspond to thinning and con-traction rule
Intersection types are an essential tool in the analysis of operational and denotational properties of lambda-terms and functional programs. Among them, non-idempotent intersection types provide precise quantitative information about the evaluation o
We study polymorphic type assignment systems for untyped lambda-calculi with effects, based on Moggis monadic approach. Moving from the abstract definition of monads, we introduce a version of the call-by-value computational lambda-calculus based on
This volume contains a final and revised selection of papers presented at the Seventh Workshop on Intersection Types and Related Systems (ITRS 2014), held in Vienna (Austria) on July 18th, affiliated with TLCA 2014, Typed Lambda Calculi and Applicati