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

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

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

(6)

• A proof of strong normalization for \(F_ 2\), \(F_ \omega\), and beyond
• Internal normalization, compilation and decompilation for System \({\mathcal F}_{\beta\eta}\)
• Typed Applicative Structures and Normalization by Evaluation for System F ω
• Internal models of system F for decompilation
• A proof of the normal form theorem for the closed terms of Girard's system F by means of computability
• Schwichtenberg's style analysis of parameter-free fragments of Girard's 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)