# Publications (or soon to be)

**Infinitary Intersection Types as Sequences: a New Answer to Klop's Question [LICS2017]**: short (05.10.2017) and long (05.03.2017) versions.

*Abstract:*We use infinite sequences to represent intersection and define a coinductive intersection type sytem that characterizes the set of weakly normalizing terms of an infinitary calculus. A finite term is normalizing in this calculus if its Böhm tree does not hold bottom.-
**Types as Resources for Classical Natural Deduction [FSCD2017, 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 [Accepted in POPL2018, 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.

# Preprints

**The Multiset-Theoretic Collapse of the Sequential Intersection Type System is Surjective**: short (05.10.2017) and long (05.10.2017) versions.

*Abstract:*The derivations of System R, whose intersection types are sequential, naturally collapses on M, 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.-
**Coinductive Types are Completely Unsound:**short (05.10.2017) and long (05.10.2017) versions.

*Abstract*: Certain type assignment systems are known to ensure or characterize normalization. The grammar of the types they feature is usually inductive. It is easy to see that, when types are coinductively generated, we obtain unsound type systems (meaning here that they are able to type some mute terms). Even more, for most of those systems, it is not difficult to find an argument proving that every term is typable (complete unsoundness). However, this argument does not hold for relevant intersection type systems (ITS), that are more restrictive because they forbid weakening. Thus, the question remains: are relevant ITS featuring coinductive types – despite being unsound – still able to characterize some bigger class of terms? We show that it is actually not the case: every term is typable in a standard coinductive ITS called D. Moreover, we prove that semantical information can be extracted from the typing derivations of D, as the order of the typed terms. Our work also implicitly provides a new non sensible relational model for pure λ-calculus.