We present a proof theoretical method for de-compiling low- level code to the typed lambda calculus. We rst de ne a proof system for a low-level code language based on the idea of Curry-Howard iso- morphism. This allows us to regard an executable code as a proof in intuitionistic propositional logic. As being a proof of intuitionistic logic, it can be translated to an equivalent proof of 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 en- coding 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 in- structions 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.