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
|
| Project Status |
Completed (Fiscal Year 2001)
|
| Budget Amount *help |
¥2,900,000 (Direct Cost: ¥2,900,000)
Fiscal Year 2001: ¥1,300,000 (Direct Cost: ¥1,300,000)
Fiscal Year 2000: ¥1,600,000 (Direct Cost: ¥1,600,000)
|
|---|
| Keywords | MACHINE CODE / LOGIC / COMPILE / DE-COMPILE / TYPE THEORY / プログラミング言語 / 機械語 / Curry-Howard同型 |
|---|
| 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.
|
Report
(3 results)
Research Products
(10 results)
