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.
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.