The logical abstract machine: A Curry-Howard isomorphism for machine code

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

9 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationFunctional and Logic Programming - 4th Fuji International Symposium, FLOPS 1999, Proceedings
EditorsAart Middeldorp, Taisuke Sato
PublisherSpringer Verlag
Pages300-318
Number of pages19
ISBN (Print)354066677X, 9783540666776
DOIs
Publication statusPublished - 1999 Jan 1
Externally publishedYes
Event4th Fuji International Symposium on Functional and Logic Programming, FLOPS 1999 - Tsukuba, Japan
Duration: 1999 Nov 111999 Nov 13

Publication series

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

Other

Other4th Fuji International Symposium on Functional and Logic Programming, FLOPS 1999
CountryJapan
CityTsukuba
Period99/11/1199/11/13

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'The logical abstract machine: A Curry-Howard isomorphism for machine code'. Together they form a unique fingerprint.

Cite this