PROOF-THEORETICAL INVESTIGATION ON MACHINE CODE AND CODE GENERATION

点击翻译按钮获取中文摘要

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.