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

reducibilitylambda-calculusChurch-Rosser propertytyped lambda-calculus

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Recommendations

• Reduction rules for intuitionistic \(\lambda\rho\)-calculus
• Publication:4945227
• 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 \(\lambda\)-calculus

Cited in

(22)

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

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)