[ Back to Ohori's research interest page | Ohori's home page | 大堀淳のホームページ (home page in Japanese) ]

Logical Foundations for Compilation, Decompilation, and Code Analysus

Parallel to the correspondence between the typed lambda calculus and the natural deduction proof system, it is possible to establish a correspondence between low-level languages (e.g. intermediate languages, bytecode code, and machine code) and proof systems of the intuitionistic propositional logic. This enables us to present compilation of the lambda calculus as a proof transformation from the natural deduction to a proof system of a low-level language. Moreover, the inverse transformation is equally possible, yielding proof-directed de-compilation of a low-level language. Based on this general observation, this research aim at establishing logical foundations for compilation, de-compilation and code analysis systems. Current specific researchs topic include the following. Contributions in these and related topics include the following. See also some slides of invited talks on related topics.
The documents contained in these directories are the author's verisons of published articles. They are included here by the author as a means to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
Atsushi Ohori / ohori@jaist.ac.jp / TEL: +81 761 51-1275