Exact Intersection Type Abstractions for Safety Checking of Recursion Schemes

Higher-order recursion schemes are a class of higher-order programs built from a collection of first-order constants using higher-order functions and general recursion. Since the trees that they define have many decidable properties, they have become widely studied in the context of the verification through higher-order model checking.