@inproceedings{35b7ead8ed4749079d099453cd0756ad,

title = "The logical abstract machine: A Curry-Howard isomorphism for machine code",

abstract = "This paper presents a logical framework for low-level machine code and code generation. We first define a calculus, called sequential sequent calculus, of intuitionistic propositional logic. A proof of the calculus only contains left rules and has a linear (non-branching) structure, which reflects the properties of sequential machine code. We then establish a Curry-Howard isomorphism between this proof system and machine code based on the following observation. An ordinary machine instruction corresponds to a polymorphic proof transformer that extends a given proof with one inference step. A return instruction, which turns a sequence of instructions into a program, corresponds to a logical axiom (an initial proof tree). Sequential execution of code corresponds to transforming a proof to a smaller one by successively eliminating the last inference step. This logical correspondence enables us to present and analyze various low-level implementation processes of a functional language within the logical framework. For example, a code generation algorithm for the lambda calculus is extracted from a proof of the equivalence theorem between the natural deduction and the sequential sequent calculus.",

author = "Atsushi Ohori",

year = "1999",

month = jan,

day = "1",

doi = "10.1007/10705424_20",

language = "English",

isbn = "354066677X",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "300--318",

editor = "Aart Middeldorp and Taisuke Sato",

booktitle = "Functional and Logic Programming - 4th Fuji International Symposium, FLOPS 1999, Proceedings",

note = "4th Fuji International Symposium on Functional and Logic Programming, FLOPS 1999 ; Conference date: 11-11-1999 Through 13-11-1999",

}