TY - JOUR

T1 - A proof theory for machine code

AU - Ohori, Atsushi

PY - 2007/10/1

Y1 - 2007/10/1

N2 - This article develops a proof theory for low-level code languages. We first define a proof system, which we refer to as the sequential sequent calculus, and show that it enjoys the cut elimination property and that its expressive power is the same as that of the natural deduction proof system. We then establish the Curry-Howard isomorphism between this proof system and a low-level code language by showing the following properties: (1) the set of proofs and the set of typed codes is in one-to-one correspondence, (2) the operational semantics of the code language is directly derived from the cut elimination procedure of the proof system, and (3) compilation and decompilation algorithms between the code language and the typed lambda calculus are extracted from the proof transformations between the sequential sequent calculus and the natural deduction proof system. This logical framework serves as a basis for the development of type systems of various low-level code languages, type-preserving compilation, and static code analysis.

AB - This article develops a proof theory for low-level code languages. We first define a proof system, which we refer to as the sequential sequent calculus, and show that it enjoys the cut elimination property and that its expressive power is the same as that of the natural deduction proof system. We then establish the Curry-Howard isomorphism between this proof system and a low-level code language by showing the following properties: (1) the set of proofs and the set of typed codes is in one-to-one correspondence, (2) the operational semantics of the code language is directly derived from the cut elimination procedure of the proof system, and (3) compilation and decompilation algorithms between the code language and the typed lambda calculus are extracted from the proof transformations between the sequential sequent calculus and the natural deduction proof system. This logical framework serves as a basis for the development of type systems of various low-level code languages, type-preserving compilation, and static code analysis.

KW - Curry-Howard isomorphism

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

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

U2 - 10.1145/1286821.1286827

DO - 10.1145/1286821.1286827

M3 - Article

AN - SCOPUS:36048966264

VL - 29

JO - ACM Transactions on Programming Languages and Systems

JF - ACM Transactions on Programming Languages and Systems

SN - 0164-0925

IS - 6

M1 - 1286827

ER -