[TYPES] Paper available: a proof theory for machine code

[Atsushi Ohori]

The following paper has been made available.  Comments and suggestions
are warmly welcome.
	  					Atsushi Ohori

A Proof Theory for Machine Code 
by Atsushi Ohori

URL:  http://www.jaist.ac.jp/~ohori/research/LogicalMachine.pdf

This paper 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 de-compilation 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.

(A preliminary summary was presented at FLOPS'99, LNCS 1722, 1999.)