Free Online Productivity Tools
i2Speak
i2Symbol
i2OCR
iTex2Img
iWeb2Print
iWeb2Shot
i2Type
iPdf2Split
iPdf2Merge
i2Bopomofo
i2Arabic
i2Style
i2Image
i2PDF
iLatex2Rtf
Sci2ools

ESOP

2001

Springer

2001

Springer

Abstract. We present a proof theoretical method for de-compiling lowlevel 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 isomorphism. 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 encoding of a sequence of primitive instructions, but reﬂects the behavior of the given program. This process therefore serves as proof-directed decompilation 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...

Added |
28 Jul 2010 |

Updated |
28 Jul 2010 |

Type |
Conference |

Year |
2001 |

Where |
ESOP |

Authors |
Shin-ya Katsumata, Atsushi Ohori |

Comments (0)