Reducibility Proofs in the λ-Calculus

DOI10.3233/FI-2012-773MaRDI QIDQ4903716zbMATH OpenOpenAlexFDO

Authors Fairouz Kamareddine, Vincent Rahli, J. B. Wells

Publication date 24 January 2013

Published in Fundamenta Informaticae (Search for Journal in Brave)

Full work available at URL https://doi.org/10.3233/fi-2012-773

zbMATH Keywords

Church-Rosser propertylambda-calculusreducibilitytyped lambda-calculus

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Recommendations

• Reduction rules for intuitionistic -calculus
• scientific article; zbMATH DE number 1424037
• Perpetual reductions in -calculus
• Refining reduction in the lambda calculus
• Term Rewriting and Applications
• The self-reduction in lambda calculus
• scientific article; zbMATH DE number 7084951
• scientific article; zbMATH DE number 1670575
• scientific article; zbMATH DE number 2134911
• Exact bounds for lengths of reductions in typed -calculus

Cited in

(26)

• Needed reduction and spine strategies for the lambda calculus
• Decidability of the restriction equational theory in the partial lambda calculus
• Typing untyped \(\lambda\)-terms, or reducibility strikes again!
• Constructive proofs of the range property in lambda calculus
• Does reductive proof theory have a viable rationale?
• An upper bound for reduction sequences in the typed -calculus
• Reducibility: a ubiquitous method in lambda calculus with intersection types
• Reduction and conversion strategies for the calculus of (co)inductive constructions. I
• scientific article; zbMATH DE number 3933030 (Why is no real title available?)
• scientific article; zbMATH DE number 176742 (Why is no real title available?)
• scientific article; zbMATH DE number 1303339 (Why is no real title available?)
• A linearization of the Lambda-calculus and consequences
• scientific article; zbMATH DE number 1499090 (Why is no real title available?)
• scientific article; zbMATH DE number 1523050 (Why is no real title available?)
• scientific article; zbMATH DE number 7029315 (Why is no real title available?)
• Theoretical PearlsEnumerators of lambda terms are reducing
• scientific article; zbMATH DE number 1868923 (Why is no real title available?)
• scientific article; zbMATH DE number 806614 (Why is no real title available?)
• Refining reduction in the lambda calculus
• scientific article; zbMATH DE number 7204561 (Why is no real title available?)
• Simplified reducibility proofs of Church-Rosser for \({\beta}\)- and \({\beta}{\eta}\)-reduction
• Formal SOS-Proofs for the Lambda-Calculus
• scientific article; zbMATH DE number 7084951 (Why is no real title available?)
• Algebra and Coalgebra in Computer Science
• On the Stability by Union of Reducibility Candidates
• Reductions for non-clausal theorem proving

This page was built for publication: Reducibility Proofs in the λ-Calculus

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