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

DOI10.1007/3-540-48959-2_20MaRDI QIDQ4263876zbMATH OpenFDO

Authors Atsushi Ohori

Publication date 21 November 1999

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-48959-2_20

zbMATH Keywords

\(A\)-normal formscompilationCurry-Howard isomorphismcuts of proofsintuitionistic sequent calculusnatural deductionprogram executionproof normalizationproof transformation

Mathematics Subject Classification ID

Logic in computer science (03B70) Cut-elimination and normal-form theorems (03F05) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• scientific article; zbMATH DE number 2063228
• The logical abstract machine: A Curry-Howard isomorphism for machine code
• scientific article; zbMATH DE number 749923
• A variadic extension of Curry's fixed-point combinator
• scientific article; zbMATH DE number 1302066
• Curry-style type isomorphisms and game semantics
• Compilation as Rewriting in Higher Order Logic
• scientific article; zbMATH DE number 5510503
• Compilation of extended recursion in call-by-value functional languages
• Abstract conjunctive partial deduction for the analysis and compilation of coroutines

Cited in

(3)

• The logical abstract machine: A Curry-Howard isomorphism for machine code
• Computing with semirings and weak rig groupoids
• scientific article; zbMATH DE number 2063228 (Why is no real title available?)

This page was built for publication: A Curry-Howard isomorphism for compilation and program execution. (Extended abstract)

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4263876)