A Curry-Howard isomorphism for compilation and program execution (Extended abstract)

被引：0

作者：

Ohori, A ^{[1
]}

机构：

[1] Kyoto Univ, Math Sci Res Inst, Kyoto 6068502, Japan

来源：

TYPED LAMBDA CALCULI AND APPLICATIONS | 1999年 / 1581卷

关键词：

D O I：

暂无

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

This paper establishes a Curry-Howard isomorphism for compilation and program execution by showing the following facts. (1) The set of A-normal forms, which is often used as an intermediate language for compilation, corresponds to a subsystem of Kleene's contraction-free variant of Gentzen's intuitionistic sequent calculus. (2) Compiling the lambda terms to the set of A-normal forms corresponds to proof transformation from the natural deduction to the sequent calculus followed by proof normalisation. (3) Execution of an A-normal form corresponds to a special proof reduction in the sequent calculus. Different from cut elimination, this process eliminates left rules by converting them to cuts of proofs corresponding to closed values. The evaluation of an entire program is the process of inductively applying this process followed by constructing data structures.

引用

页码：280 / 294

页数：15