Types and higher-order recursion schemes for verification of higher-order programs

We propose a new verification method for temporal properties of higher-order functional programs, which takes advantage of Ong's recent result on the decidability of the model-checking problem for higher-order recursion schemes (HORS's). A program is trans- formed to an HORS that generates a tree representing all the possi- ble event sequences of the program, and then the HORS is model- checked. Unlike most of the previous methods for verification of higher-order programs, our verification method is sound and com- plete. Moreover, this new verification framework allows a smooth integration of abstract model checking techniques into verification of higher-order programs. We also present a type-based verification algorithm for HORS's. The algorithm can deal with only a frag- ment of the properties expressed by modal μ-calculus, but the al- gorithm and its correctness proof are (arguably) much simpler than those of Ong's game-semantics-based algorithm. Moreover, while the HORS model checking problem is n-EXPTIME in general, our algorithm is linear in the size of HORS, under the assumption that the sizes of types and specifications are bounded by a constant.