Proof-directed de-compilation of low-level code

Shin Ya Katsumata, Atsushi Ohori

研究成果: Conference contribution

12 被引用数 (Scopus)

抄録

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.

本文言語English
ホスト出版物のタイトル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
編集者David Sands
出版社Springer Verlag
ページ352-366
ページ数15
ISBN(印刷版)3540418628
DOI
出版ステータスPublished - 2001
イベント10th European Symposium on Programming, ESOP 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 - Genova, Italy
継続期間: 2001 4 22001 4 6

出版物シリーズ

名前Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
2028
ISSN(印刷版)0302-9743
ISSN(電子版)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)

フィンガープリント 「Proof-directed de-compilation of low-level code」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル