In this talk, we present an original coinductive type system, that we call S (S standing for "Sequence"). This system features intersection types that are sequence of types, instead of sets or multisets of types as in other framework. We develop a few applications of this type System.

• A new answer to Klop's Question: in the early 90, Klop asked whether the set of hereditary head-normalizable terms could be characterized by type assignments. Tatsuta [07] showed that this was not possible with inductive type systems. We prove here that System S can answer positively to Klop's Question, provided we endow it with a validity condition (meant to discard some unsound proofs) that we call approximability.

• A semantic for pure lambda-calculus: if we forget about the aforementioned validity criterion, we show that every term is typable in system S. Collapsing sequences on multisets, this provides a new model for pure lambda-calculus that does not equate all the non terminating terms (such a model is called non-sensible). One of the important feature of this model is that is gives a non-empty denotation to every term, including the most irregular ones (the so-called mute terms), and is able to discriminate terms according to their order (the number of abstractions that may prefix a term).

• The surjectivity of the collapse of S on R: we show that every derivation of the infinitary version of Gardner/de Carvalho's System R (featuring multiset intersection) is the collapse of a derivation of S.