*Semantics Club 23 03 2001*

# Proof-Directed De-compilation of Low-Level Code

(joint work with Atushi Ohori)### Abstract

We present a proof theoretical method for de-compiling low-level code to the typed lambda
calculus. We first define a proof system for a low-level code language based on the idea of
Curry-Howard isomorphism. This allows us to regard an executable code as a proof of the
intuitionistic propositional logic. As being a proof of the intuitionistic logic, it can be
translated to an equivalent proof of the natural deduction proof system. This property yields
an algorithm to translate a given code into a lambda term. Moreover, the resulting lambda
term is not a trivial encoding of a sequence of primitive instructions, but reflects the behavior
of the given program. This process therefore serves as proof-directed de-compilation of a
low-level code language to a high-level language. We carry out this development for a
subset of Java Virtual Machine instructions including most of its features such as jumps,
object creation and method invocation. The proof-directed de-compilation algorithm has
been implemented, which demonstrates the feasibility of our approach.
**This talk will also be given in ESOP'01. Comments are welcome.**