A type system equivalent to the modal Mu-calculus model checking of higher-order recursion schemes

The model checking of higher-order recursion schemes has important applications in the verification of higher-order programs. Ong has previously shown that the modal mu-calculus model checking of trees generated by ordern recursion scheme is n-EXPTIME complete, but his algorithm and its correctness...