Proof-directed de-compilation of low-level code

Shin Ya Katsumata, Atsushi Ohori

Research output: Chapter in Book/Report/Conference proceedingConference contribution

12 Citations (Scopus)

Abstract

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.

Original languageEnglish
Title of host publicationProgramming 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
EditorsDavid Sands
PublisherSpringer Verlag
Pages352-366
Number of pages15
ISBN (Print)3540418628
DOIs
Publication statusPublished - 2001
Event10th European Symposium on Programming, ESOP 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 - Genova, Italy
Duration: 2001 Apr 22001 Apr 6

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2028
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other10th European Symposium on Programming, ESOP 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001
CountryItaly
CityGenova
Period01/4/201/4/6

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Proof-directed de-compilation of low-level code'. Together they form a unique fingerprint.

Cite this