Although the following abstract is (mostly) in French, the talk will be in English if there are non-French speakers in the room.

L'exposé aura deux buts:

1) Présenter les systèmes de types-intersection (ITS, intersection type
systems), en particulier, les ITS à intersection non-idempotente.
Je commencerai par des rappels basiques en lambda-calcul. On verra en
quoi la représentation des lambda-termes par des arbres (bien
qu'élémentaire) permet de comprendre la façon dont les ITS sont conçus
et vérifient naturellement des propriétés que les systèmes de types
simples ne peuvent (raisonnablement) pas avoir. Par exemple, dans un
ITS, un terme est normalisable (i.e. il termine) ssi il est typable. Par
opposition, dans un système de types simples, on aura seulement
l'implication "Si le terme t est typable, alors il est normalisable"
(*Propriété de Terminaison*). La notion de normalisation (i.e.
terminaison) admet de nombreuses variantes: on en verra deux, la
réduction de tête (HN, Head Normalization) et la réduction faible (WN,
Weak Normalization). On verra aussi que les ITS ont des conséquences en
lambda-calcul qui sont *externes* à la théorie des types.

Etant donné un système de type Sys (que Sys soit un ITS ou un système de
types simples, d'ordre supérieur ou non), la propriété de terminaison
(typable dans Sys => normalisable) est souvent difficile à établir (on
doit généralement recourir à un argument dit de réalisabilité, attribué
à Tait). Cependant, je présenterai le système R, introduit par Gardner
et de de Carvalho, dans lequel l'opérateur d'intersection peut être vu
comme non-idempotent et la terminaison repose sur un argument très
simple que nous verrons ensemble.


2) Présenter un article (accepté récemment à LICS) traitant de
lambda-calcul et de réduction infinitaires et dont voici l'abstract:

Infinitary Intersection Types as Sequences: a New Answer to Klop’s Problem

We provide a type-theoretical characterization of weakly-normalizing
terms in an infinitary lambda-calculus. We adapt for this purpose the
standard quantitative (with non-idempotent intersections) type
assignment system of the lambda-calculus to our infinite calculus.
Our work provides a positive answer to a semi-open question known as
Klop’s Problem, namely, finding out if there is a type system
characterizing the set of hereditary head-normalizing (HHN)
lambda-terms. Tatsuta showed in 2007 that HHN could not be characterized
by a finite type system. We prove that an infinitary type system endowed
with a validity condition called approximability can achieve it.
As it turns out, approximability cannot be expressed when intersection
is represented by means of multisets. Multisets are then replaced
coinductively by sequences of types indexed by integers, thus defining a
type system called System S.