PROOF-THEORETICAL INVESTIGATION ON MACHINE CODE AND CODE GENERATION

本研究的目的是建立机器码的证明理论解释，并发展一套系统的机器码产生与分析方法。通过本课题的研究，我们取得了以下三个方面的成果。(1)低级机器中的每条指令都可以被重新分级为一个左规则，在一个类证明系统中只有一个前提。基于这一观察，我们已经开发了一个证明系统，称为序贯演算，机器代码，并开发了一个编译算法作为证明转换从自然演绎证明系统，这个演算。(2)应用上述结果，我们建立了Java字节码语言的一个证明系统，并证明了Java字节码与lambda演算之间的转换是可能的。Mycroft，我们比较了我们的机器代码分析的证明导向框架和Mycroft的基于类型的框架，并表明这两个框架是复杂的，证明导向框架在分析代码的控制信息方面能力更强，而基于类型的分析对于分析具有多个类型的通用指令是必要的。

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.