A curry-howard isomorphism for compilation and program execution

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

6 Citations (Scopus)

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’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 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.

Original languageEnglish
Title of host publicationTyped Lambda Calculi and Applications - 4th International Conference, TLCA 1999, Proceedings
EditorsJean-Yves Girard
PublisherSpringer-Verlag
Pages280-294
Number of pages15
ISBN (Print)3540657630, 9783540657637
Publication statusPublished - 1999 Jan 1
Externally publishedYes
Event4th International Conference on Typed Lambda Calculi and Applications, TLCA 1999 - L’Aquila, Italy
Duration: 1999 Apr 71999 Apr 9

Publication series

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

Other

Other4th International Conference on Typed Lambda Calculi and Applications, TLCA 1999
Country/TerritoryItaly
CityL’Aquila
Period99/4/799/4/9

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'A curry-howard isomorphism for compilation and program execution'. Together they form a unique fingerprint.

Cite this