Automating relatively complete verification of higher-order functional programs, 2012. http: //www.kb.is.s.u-tokyo.ac.jp/~uhiro/relcomp

We present an automated approach to relatively completely veri-fying safety (i.e., reachability) property of higher-order functional programs. Our contribution is two-fold. First, we extend the refine-ment type system framework employed in the recent work on (in-complete) automated higher-order verification by drawing on the classical work on relatively complete “Hoare logic like ” program logic for higher-order procedural languages. Then, by adopting the recently proposed techniques for solving constraints over quanti-fied first-order logic formulas, we develop an automated type infer-ence method for the type system, thereby realizing an automated relatively complete verification of higher-order programs