  Higher-order recursion schemes are a higher-order analogue of Boolean
Programs; they form a natural class of abstractions for functional programs. We
present a new, efficient algorithm for checking CTL properties of the trees
generated by higher-order recursion schemes, which is an extension of
Kobayashi's intersection type-based model checking technique. We show that an
implementation of this algorithm, THORS, performs well on a number of small
examples and we demonstrate how it can be used to verify liveness properties of
OCaml programs. Example properties include statements such as "all opened
sockets are eventually closed" and "the lock is held until the file is closed".
