The Logical Abstract Machine: A Curry-Howard Isomorphism for Machine Code
The Logical Abstract Machine: A Curry-Howard Isomorphism for Machine Code
复制标题
逻辑抽象机：机器代码的柯里-霍华德同构
DOI：
--
复制
发表时间：
1999
期刊：
影响因子：
--
通讯作者：
A. Ohori
中科院分区：
文献类型：
--
作者：
A. Ohori
本文提出了一个用于低级机器码和代码生成的逻辑框架。我们首先定义直觉命题逻辑的一种演算，称为序贯演算。微积分的证明只包含左规则，并且具有线性（无分支）结构，反映了顺序机器码的性质。然后，基于以下观察，我们在该证明系统和机器码之间建立了Curry-Howard同构。一个普通的机器指令对应于一个多态证明转换器，该转换器用一个推理步骤扩展给定的证明。返回指令将指令序列转换为程序，对应于逻辑公理（初始证明树）。代码的顺序执行对应于通过依次消除最后一个推理步骤将证明转换为较小的证明。这种逻辑对应使我们能够在逻辑框架内呈现和分析函数式语言的各种低级实现过程。例如，lambda演算的代码生成算法是从自然演绎和顺序演算之间的等价定理的证明中提取出来的。
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.