scientific article; zbMATH DE number 806614

zbMATH Open0830.03003MaRDI QIDQ4850465FDOQ4850465

Authors: René David 

Publication date: 21 November 1995

Title of this publication is not available (Why is that?)

Recommendations

• Church–Rosser Made Easy
• Fundamental theorems of extensional untyped \(\lambda\)-calculus revisited
• scientific article; zbMATH DE number 7106482
• Reducibility Proofs in the λ-Calculus
• A direct proof of the finite developments theorem

zbMATH Keywords

lambda calculusChurch-Rosser theoremfiniteness of developments theoremstandardisation theoremstrong normalisation theorem

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Cited In (16)

• Title not available (Why is that?)
• Statman's 1-section theorem
• A syntactic proof of the conservativity of \(\lambda_\omega\) over \(\lambda_2\)
• Parametric parameter passing \(\lambda\)-calculus
• A direct proof of the confluence of combinatory strong reduction
• A direct proof of the finite developments theorem
• [Russian Text Ignored]
• Analytic proof systems for \(\lambda\)-calculus: the elimination of transitivity, and why it matters
• Fundamental theorems of extensional untyped \(\lambda\)-calculus revisited
• Church meets Cook and Levin
• Some properties of the \(\lambda\mu^{\wedge\vee}\)-calculus
• New proofs of important theorems of untyped extensional \(\lambda\) calculus
• The mechanisation of Barendregt-style equational proofs (the residual perspective)
• Normalization without reducibility
• A lambda proof of the P-W theorem
• Parallel reductions in \(\lambda\)-calculus

This page was built for publication:

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