An elementary proof of the normalization theorem for -reduction

MaRDI QIDQ2933396zbMATH OpenFDO

Authors O. O. Lyalets'kyj

Publication date 10 December 2014

zbMATH Keywords

lambda calculusnormalization theorem\(\beta\eta\)-reductionleftmost strategy

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Recommendations

• A proof of the leftmost reduction theorem for -calculus
• New proofs of important theorems of untyped extensional \(\lambda\) calculus
• scientific article; zbMATH DE number 512779
• Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters
• Fundamental theorems of extensional untyped \(\lambda\)-calculus revisited

Cited in

(3)

• A proof of the leftmost reduction theorem for \(\lambda\beta\eta\)-calculus
• New proofs of important theorems of untyped extensional \(\lambda\) calculus
• scientific article; zbMATH DE number 7039354 (Why is no real title available?)

This page was built for publication: An elementary proof of the normalization theorem for \(\beta\eta\)-reduction

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