2009 Fiscal Year Final Research Report
Research on program transformation systems based on automated theorem proving
| Project/Area Number |
19500003
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
TOYAMA Yoshihito Tohoku University, 電気通信研究所, 教授 (00251968)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
AOTO Takahito 東北大学, 電気通信研究所, 准教授 (00293390)
|
|---|
| Project Period (FY) |
2007 – 2009
|
| Keywords | プログラム理論 / プログラム変換 |
|---|
| Research Abstract |
The theory of term rewriting systems is widely used in the fields of automated theorem provings and computation models. This research aims to develop basic theories and prototypes for automated program transformation systems based on term rewriting theory. Concrete results include an automated construction method of program transformation templates, a new termination proof of higher-order programs, an automated lemma generation method for rewriting induction, an automated confluence prover of term rewriting systems.
|
