Pumping by Typing

Higher-order recursion schemes (HORS), which are higher-order grammars for generating infinite trees, have recently been studied extensively in the context of model checking and its applications to higher-order program verification. We develop a pumping lemma for HORS by using a novel but simple intersection type system for reasoning about reductions of λ-terms. Our proof is arguably much simpler than the proof of Kartzow and Parys´ pumping lemma for collapsible pushdown automata. As an application, we give an alternative proof of Kartzow and Parys´ result about the strictness of the hierarchy of trees generated by HORS.