Tags:higher order recursion schemes, intersection types and unboundedness

Abstract:

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.

Intersection Types for Unboundedness Problems (ITRS invited talk)