Research Areas
- Term Rewriting
- Automated Theorem Proving
- Foundations of Software
Overview
Our research goal is to understand various aspects of computations as well as to apply such understanding in verifications and constructions of software. For this, we investigate theories and applications of formal models of computation. In particular, we focus on term rewriting which is such a model based on equational logic. All in all, we aim at contributing to establish a new paradigm of software technologies based on mathematical logic and computer science.
Research Topics
Rewriting via equations is our familiar mathematical inference method, which is not only easy to understand for everyone but also both flexible and effective. Such a method of computation has been also adapted in various applications in computer science and software technologies. Our research topic is around such a method of computation, formally called term rewriting. Thus, we are interested in various aspects of computations by rewriting, automated verification of various properties of rewrite systems, and their applications in verifying and sophisticating programs by formal methods.