Weak βη-Normalization and Normalization by Evaluation for System F

DOI10.1007/978-3-540-89439-1_35MaRDI QIDQ5505577zbMATH OpenOpenAlexFDO

Authors Andreas Abel

Publication date 27 January 2009

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.575.5430

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Logic in computer science (03B70)

Recommendations

• scientific article; zbMATH DE number 4134006
• Internal normalization, compilation and decompilation for System \({\mathcal F}_{\beta\eta}\)
• Typed Applicative Structures and Normalization by Evaluation for System F ω
• scientific article; zbMATH DE number 512769
• A proof of the normal form theorem for the closed terms of Girard's system F by means of computability

Cited in

(4)

• Internal models of system F for decompilation
• Internal normalization, compilation and decompilation for System \({\mathcal F}_{\beta\eta}\)
• A proof of the normal form theorem for the closed terms of Girard's system F by means of computability
• Typed Applicative Structures and Normalization by Evaluation for System F ω

This page was built for publication: Weak βη-Normalization and Normalization by Evaluation for System F

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