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 transformed to an HORS that generates a tree representing all the possible event sequences of the program, and then the HORS is modelchecked. Unlike most of the previous methods for verification of higher-order programs, our verification method is sound and complete. Moreover, this new verification framework allows a smooth ion 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 fragment of the properties expressed by modal -calculus, but the algorithm and its correctness proof are (arguably) much simpler than those of Ong's game-semantics-based algorithm. Moreover, while the HORS model check...

• Type: Conference
• Year: 2009
• Where: POPL
• Authors: Naoki Kobayashi
• Keywords: Game-semantics-based Algorithm, HORS Model, POPL 2009, Programming Languages, Type-based Verification Algorithm