2001 Fiscal Year Final Research Report Summary
PROOF-THEORETICAL INVESTIGATION ON MACHINE CODE AND CODE GENERATION
| Project/Area Number |
12680345
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
OHORI Atsushi Japan Advanced Institute of Science and Technology, Professor, 情報科学研究科, 教授 (60252532)
|
|---|
| Project Period (FY) |
2000 – 2001
|
| Keywords | MACHINE CODE / LOGIC / COMPILE / DE-COMPILE / TYPE THEORY |
|---|
| Research Abstract |
The purpose of this research is to establish proof-theoretical interpretation of machine code, and to develop a systematic methods for code generation and code analysis. Through this research project, we have obtained the following three results.
(1) Each instruction in a low-level machine can be regraded as a left rule with only one premise in a sequent style proof system. Based on this observation, we have developed a proof system, called sequential sequent calculus, for machine code and have developed a compilation algorithm as a proof transformation from the natural deduction proof system to this calculus.
(2) By applying the above results, we have established a proof system for Java bytecode language, and have show that it is possible to transform between Java bytecode and the lambda calculus,
(3) Jointly with A. Mycroft, we have compared our proof-directed framework for machine code analysis with the type-based framework of Mycroft, and have shown that these two frameworks are comple mentary - proof-directed framework is stronger in its ability to analyze control information of code while the type based analysis is necessary for analyzing generic instructions having multiple types.
|
