Refining reduction in the lambda calculus

DOI10.1017/S0956796800001507zbMATH Open0846.68057OpenAlexW2118527795MaRDI QIDQ4880488FDOQ4880488

Rob Nederpelt, Fairouz Kamareddine

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

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 (18)

• 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
• 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
• Title not available (Why is that?)
• Title not available (Why is that?)
• Needed reduction and spine strategies for the lambda calculus
• Parallel reductions in \(\lambda\)-calculus

Recommendations

• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Title not available (Why is that?) 👍 👎
• Term Rewriting and Applications 👍 👎
• Reduction graphs in the lambda calculus 👍 👎
• Combinatory weak reduction in lambda calculus 👍 👎
• The self-reduction in lambda calculus 👍 👎
• Reducibility Proofs in the λ-Calculus 👍 👎
• Reducibility: a ubiquitous method in lambda calculus with intersection types 👍 👎
• Demonstrating Lambda Calculus Reduction 👍 👎

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)