TY - GEN

T1 - Proof-directed de-compilation of low-level code

AU - Katsumata, Shin Ya

AU - Ohori, Atsushi

N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2001.

PY - 2001

Y1 - 2001

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84945274223&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84945274223&partnerID=8YFLogxK

U2 - 10.1007/3-540-45309-1_23

DO - 10.1007/3-540-45309-1_23

M3 - Conference contribution

AN - SCOPUS:84945274223

SN - 3540418628

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 352

EP - 366

BT - Programming Languages and Systems - 10th European Symposium on Programming, ESOP 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001, Proceedings

A2 - Sands, David

PB - Springer Verlag

T2 - 10th European Symposium on Programming, ESOP 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001

Y2 - 2 April 2001 through 6 April 2001

ER -