Seminars & WorkshopsTypes and Recursion Schemes for HigherOrder Program Verification
AbstractHigherorder recursion schemes (recursion schemes, for short) are expressive grammars for describing infinite trees. The modal µcalculus model checking problem for recursion schemes (“Given a recursion scheme G and a modal µcalculus formula phi, does the tree generated by G satisfy phi?”) has been a hot research topic in the theoretical community for recent years. In 2006, it has been shown to be decidable, and nEXPTIME complete (where n is the order of a recursion scheme) by Ong. The model checking of recursion schemes has recently turned out to be a good basis for verification of higherorder functional programs, just as finite state model checking for programs with whileloops, and pushdown model checking for programs with firstorder recursion. First, various program analysis/verification problems such as reachability, flow analysis, and resource usage verification (or equivalently, typestate checking) can be easily transformed into modelchecking problems for recursion schemes. Combined with a model checking algorithm for recursion schemes, this yields a sound, complete, and automated verification method for the simplytyped λcalculus with recursion and finite base types such as booleans. Secondly, despite the extremely high worstcase time complexity (i.e. nEXPTIME completeness) of the model checking problem for recursion schemes, our typebased modelchecking algorithm turned out to run reasonably fast for realistic programs. We have implemented a prototype model checker for recursion schemes TRecS, and are currently working to construct a software model checker for a subset of ML on top of it. The talk will summarize our recent results on the model checking of recursion schemes as well as its applications to higherorder program verification, and discuss future perspectives. Short bioProf. in Graduate School of Information Sciences, Tohoku Univ., Japan Ph.D. at Univ. of Tokyo Resources 
This will be shown to users with no Flash or Javascript.
