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
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.
- Logic for security analysis for low-level code
- Proof-Directed Register Allocation
- Proof-Directed Compilation
See also some slides of invited talks on related topics.
Register Allocation by Proof Transformation.
A revise version to appear in Proc. ESOP Symposium, April 2003.
slides of a preliminary talk at INRIA, 2003..
Shin-ya Katsumata and Atsushi Ohori.
Proof-Directed De-compilation of Low-level Code
Proc. ESOP Conference, 2001, Geneva, Italy.
Tomoyuki Higuchi, Atsushi Ohori
Java Bytecode as a Typed Term Calculus.
Proc. ACM PPDP conference, 2002.
The Logical Abstract Machine: a Curry-Howard isomorphism for machine code
Proc. Fuji International Symposium on Functional and Logic Programming,
Springer LNCS, November, 1999 (invited paper).
A Curry-Howard isomorphism for compilation and program execution
Proc. TLCA Conference, Springer LNCS 1581, April 1999.
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
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 / firstname.lastname@example.org / TEL: +81 761 51-1275