Current Research

Automatic Program Verification

Through the remarkable development of the computer, we can do calculations that cannot be done at all easily by hand. On the other hand, the computer cannot prove properties even if the proof can be easily done by a person with little mathematical skill. This is because not only simple calculation power but also certain sensibilities are needed to complete a proof. The study of automatic theorem proving is aimed toward bridging"calculation"and"proof". As an especially interesting application, we have studied program verification. This is because the various concepts needed when a program is verified can be formulated as a certain kind of mathematical theorem. In the following, we introduce each research topic.
■Computation Model
A term rewriting system (TRS) can be used as a computational model of functional programming languages, in which the introduction of higher-order functions consisting of arguments and values achieves a high level of abstraction and increases the expressive power. A TRS, however, cannot directly handle higher-order functions, which makes it difficult to use accumulated results in the automatic verification of functional programs. Against this background, research on higherorder rewriting systems that can handle higher-order functions has been actively studied. This research, however, has come to place a priority on theoretical interests, which has resulted in formalizations having excessive expressive power when viewed as a model of functional programming languages. With this in mind, we have proposed a simply-typed term rewriting system (STRS) as a higher-order rewriting system having sufficient expressive power for giving operational meaning to functional programming languages while still being easy to handle theoretically.
■Proving Termination of Programs
In recent years, a method for automatically proving termination of TRSs, called the dependency pair method, has been proposed by Arts and Giesl. This method analyzes the recursive structure by the function-call dependency relationship in order to prove termination. We extend the dependency pair method to STRSs, which handle higher-order functions.
We have enhanced the dependency pair method by applying the notion of strong computability, which was introduced for proving the termination of typed λ-calculus and is a stronger property than the termination. The primary advantage of our method is that one can avoid analyzing higher-order variables, which are difficult to analyze theoretically. This method is very powerful, and it can actually prove the termination of most nonartificial functional programs.
■Higher-Order Knuth-Bendix Procedure and Its Applications
The complete (i.e. confluent and terminating) property is an important concept. Knuth and Bendix have proposed a procedure known as the KB procedure for generating a complete TRS. We have proposed a higher-order KB procedure that extends the KB procedure to the framework of STRSs. We are currently studying the application of this higher-order KB procedure to a certification technique called inductionless induction, which is used in program verification.
Since our higher-order KB procedure can directly handle higher-order functions, we expect our study to contribute to the design of high confidence software.