@inproceedings{6cb0c80d83a94b6aac90a4303fec1949,

title = "A curry-howard isomorphism for compilation and program execution",

abstract = "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{\textquoteright}s contraction-free variant of Gentzen{\textquoteright}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 normalization. (3) Execution of an A-normal form corresponds to a special proof reduction in the sequent calculus. Dierent 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.",

author = "Atsushi Ohori",

year = "1999",

month = jan,

day = "1",

language = "English",

isbn = "3540657630",

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

publisher = "Springer-Verlag",

pages = "280--294",

editor = "Jean-Yves Girard",

booktitle = "Typed Lambda Calculi and Applications - 4th International Conference, TLCA 1999, Proceedings",

note = "4th International Conference on Typed Lambda Calculi and Applications, TLCA 1999 ; Conference date: 07-04-1999 Through 09-04-1999",

}