[ The Types Forum (announcements only), http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Dear All, We would like to announce a series of papers on model-checking of higher-order functional programs. The papers are available from http://www.kb.ecei.tohoku.ac.jp/~koba/publications.html. The first paper [1], presented at POPL 2009, shows that verification of temporal properties of functional programs can be reduced to model-checking problems of higher-order recursion schemes (which themselves are kind of higher-order functional programs that have tree constructors but not destructors). In the second part, it also shows that, for safety properties, model-checking problems of higher-order recursion schemes can be reduced to type-checking problems. The second paper [2] extends the second part of [1], by giving a type system equivalent to the full modal mu-calculus model-checking of recursion schemes. This provides an alternative proof of the decidability of modal mu-calculus checking of recursion schemes, which was first shown by Luke Ong in 2006 by using game semantics. The third paper [3], to be presented at ICALP 2009 next week, studies the complexity of model-checking of recursion schemes for fragments of the modal mu-calculus. Finally, the fourth paper [4] presents an optimized type-based model-checking algorithm for recursion schemes, and reports the first implementation of a model checker for recursion schemes (for safety properties). Despite n-EXPTIME-completeness of the modal mu-calculus model-checking problem of recursion schemes, the paper reports that the model-checker runs reasonably fast for a number of examples. [1] Naoki Kobayashi, "Types and Higher-Order Recursion Schemes for Verification of Higher-Order Programs", Proceedings of POPL 2009, pp.416-428, 2009. [2] Naoki Kobayashi and Luke Ong, "A Type System Equivalent to Modal Mu-Calculus Model Checking of Recursion Schemes", To appear in LICS 2009. [3] Naoki Kobayashi and Luke Ong, "Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus". To appear in ICALP 2009. [4] Naoki Kobayashi, "Model-Checking Higher-Order Functions", To appear in PPDP 2009. Best regards, Naoki Kobayashi Tohoku University