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...
| Main Authors: | , |
|---|---|
| 格式: | Conference item |
| 出版: |
2009
|