[TYPES/announce] papers on model-checking higher-order programs

[koba@kb.ecei.tohoku.ac.jp]

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