Types as Resources for Classical Natural Deduction [FSCD17, with Delia Kesner]:
short version. Abstract: We define two resource aware typing systems for the λ μ -calculus based on non-idempotent intersection and union types. The non-idempotent approach provides very simple combinatorial arguments - based on decreasing measures of type derivations– to characterize head and strongly normalizing terms. Moreover, typability provides upper bounds for the length of head-reduction sequences and maximal reduction sequences.
A longer version of this paper is available on Delia's page.
Polyadic Approximations, Fibrations and Intersection Types [POPL18, with Damiano Mazza and Luc Pellissier]:
Starting from an exact correspondence between linear approximations and non-idempotent intersection types, we develop a general framework for building systems of intersection types characterizing normalization properties. We show how this construction, which uses in a fundamental way Melliès and Zeilberger’s “type systems as functors” viewpoint, allows us to recover equivalent versions of every well known intersection type system (including Coppo and Dezani’s original system, as well as its non-idempotent variants independently introduced by Gardner and de Carvalho). We also show how new systems of intersection types may be built almost automatically in this way.
Every term is meaningful in the infinitary relation model [LICS18] Infinite types and formulas are known to have really curious and unsound behaviors. For instance, they allow to type Omega, the auto-autoapplication and they thus do not ensure any form of normalization/productivity. Moreover, in most infinitary frameworks, it is not difficult to define a type R that can be assigned to every lambda-term. However, these observations do not say much about what coinductive (i.e. infinitary) type grammars are able to provide: it is for instance very difficult to know what types (besides $R$) can be assigned to a given term in this setting. We begin with a discussion on the expressivity of different forms of infinite types.
%We see that the non-idempotent intersection types, whose resource-awareness makes them the good framework to study infinitary typing.
Then, using the resource-awareness of sequential intersection types (system S) and tracking, we prove that infinite types are able to characterize the arity of every lambda-term and that, in the infinitary extension of the relational model, every term has a ``meaning'' i.e. a non-empty denotation. From the technical point of view, we must deal with the total lack of guarantee of productivity for typable terms: we do so by importing methods inspired by first order model theory.
Reduction paths without permutations, or the expressive power of sequence types (outdated long (05.10.2017) version here). Abstract: The derivations of System S, whose intersection types are sequential, naturally collapses on R, the coinductive version of Gardner/de Carvalho's quantitive type system, featuring multisets as intersection type. We prove that this collapse is surjective : every derivation of R is the collapse of a derivation of S and we prove that we can capture every reduction path.