Refining reduction in the lambda calculus

DOI10.1017/S0956796800001507zbMATH Open0846.68057OpenAlexW2118527795MaRDI QIDQ4880488FDOQ4880488

Authors: Fairouz Kamareddine, Rob Nederpelt 

Publication date: 5 June 1996

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1017/s0956796800001507

Recommendations

• The self-reduction in lambda calculus
• scientific article; zbMATH DE number 1868923
• Combinatory weak reduction in lambda calculus
• scientific article; zbMATH DE number 1953288
• Demonstrating Lambda Calculus Reduction
• scientific article; zbMATH DE number 7084951
• Reducibility Proofs in the λ-Calculus
• Reduction graphs in the lambda calculus
• Term Rewriting and Applications
• Reducibility: a ubiquitous method in lambda calculus with intersection types

zbMATH Keywords

Church Rosser property

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

Cites Work

• Using types as search keys in function libraries
• Needed reduction and spine strategies for the lambda calculus
• A unified approach to type theory through a refined \(\lambda\)-calculus
• ON STEPWISE EXPLICIT SUBSTITUTION

Cited In (23)

• THE SOUNDNESS OF EXPLICIT SUBSTITUTION WITH NAMELESS VARIABLES
• Title not available (Why is that?)
• Canonical typing and ∏-conversion in the Barendregt Cube
• A unified approach to type theory through a refined \(\lambda\)-calculus
• Toward a reduction system commuting with beta reduction in the partial lambda calculus
• On \(\Pi\)-conversion in the \(\lambda\)-cube and the combination with abbreviations
• Generalized finite developments
• \(\rightthreetimes\)
• De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: the untyped case
• Strong normalization from weak normalization in typed \(\lambda\)-calculi
• Title not available (Why is that?)
• A list-oriented extension of the lambda-calculus satisfying the Church-Rosser theorem
• Title not available (Why is that?)
• \(\lambda_{\beta'}\) -- a \(\lambda\)-calculus with a generalized \(\beta\)-reduction rule
• Shrinking lambda expressions in linear time
• Reducibility Proofs in the λ-Calculus
• Reduction graphs in the lambda calculus
• Title not available (Why is that?)
• Title not available (Why is that?)
• Needed reduction and spine strategies for the lambda calculus
• Title not available (Why is that?)
• Title not available (Why is that?)
• Parallel reductions in \(\lambda\)-calculus

This page was built for publication: Refining reduction in the lambda calculus

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