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...
| Váldodahkkit: | , |
|---|---|
| Materiálatiipa: | Conference item |
| Almmustuhtton: |
2009
|