Intersection types have been originally developed as an extension of 
simple types, but they can also be used for refining simple types. In this 
talk we concentrate on the latter option; more precisely, on the use of 
intersection types in the context of higher-order recursion schemes. 
Intersection types were used in this context for several purposes like 
model-checking, pumping, transformations of schemes, etc. After an 
overview, I will show how intersection types can be used to solve problems 
talking about unboundedness of some quantities. An example of such a 
problem is: given a higher-order recursion scheme generating an infinite 
tree, decide whether for every number n there is a path in this tree 
containing at least n occurrences of a fixed letter #. Notice that this is 
not a regular property of the tree, thus it cannot be decided using 
standard model-checking methods.