Copenhagen Programming Language Seminar
higher-order programs, where higher-order programs are first
transformed into higher-order recursion schemes, and then
model-checked. This verification method is sound, complete, and fully
automated for the simply-typed lambda calculus with recursion and
finite data domains. A significant challenge to enable this approach
is to develop an efficient model checking algorithm for higher-order
recursion schemes. In the talk, we show that the model checking of
higher-order recursion schemes can be reduced to a type checking
problem for an intersection type system, and use this reduction to
derive a practical model checking algorithm for higher-order recursion
schemes. Based on the algorithm, we have developed TRecS, the first
model checker for higher-order recursion schemes. Despite the
extremely high worst-case complexity, TRecS is surprisingly fast for
realistic inputs, and works well as a backend of our verification
tools for functional programs. We also mention certain limitations of
our model checking algorithm, and discuss ongoing and future work to
overcome those limitations.
A part of this work has been done in collaboration with Luke Ong.
Naoki Kobayashi is a professor of Computer Science at Tohoku
University. He received his PhD from University of Tokyo in 1996.
After working as a full-time lecturer at University of Tokyo (1996-
2000), and an associate professor at Tokyo Institute of Technology
(2001-2004), he moved to Tohoku University in 2004. His research
interests are in principles of programming languages, in particular,
type systems, program verification, and concurrency.
Scientific host: Fritz Henglein, email@example.com
Administrative host: Jette Møller, firstname.lastname@example.org
Fritz Heinglein Administrative host:Jette
All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, ITU and RUC.
COPLAS is sponsored by the FIRST Graduate School.
To receive information about COPLAS talks by email, send a message to email@example.com with the word 'subscribe' as subject or in the body.
For more information about COPLAS, see http://www.coplas.org