PROOF-THEORETICAL INVESTIGATION ON MACHINE CODE AND CODE GENERATION

这项研究的目的是建立机器代码的证明论解释，并发展一套系统的代码生成和代码分析方法。通过本课题的研究，我们得到了以下三个结果：(1)在顺序风格证明系统中，低级机器上的每条指令都可以归类为只有一个前提的左规则。基于这一观察，我们开发了一个机器代码的证明系统，称为顺序顺序演算，并开发了一个编译算法作为从自然演绎证明系统到这个演算的证明转换。(2)应用上述结果，我们建立了Java字节码语言的证明系统，并证明了Java字节码和lambda演算之间的转换是可能的。(3)我们与A.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.