Abstract. We propose a new method to verify that a higher-order, treeprocessing functional program conforms to an input/output specification. Our method reduces the verification pr...
Ong has shown that the modal mu-calculus model checking problem (equivalently, the alternating parity tree automaton (APT) acceptance problem) of possibly-infinite ranked trees gen...
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 mode...