Refining reduction in the lambda calculus

DOI10.1017/S0956796800001507MaRDI QIDQ4880488zbMATHOpenAlexFDO

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

zbMATH Keywords

Church Rosser property

Mathematics Subject Classification ID

Formal languages and automata (68Q45)

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

Cites work

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

Cited in

(25)

• \(\rightthreetimes\)
• scientific article; zbMATH DE number 1868923 (Why is no real title available?)
• scientific article; zbMATH DE number 32501 (Why is no real title available?)
• Canonical typing and ∏-conversion in the Barendregt Cube
• The soundness of explicit substitution with nameless variables
• Parallel reductions in \(\lambda\)-calculus
• scientific article; zbMATH DE number 1547348 (Why is no real title available?)
• De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: the untyped case
• scientific article; zbMATH DE number 7084951 (Why is no real title available?)
• Toward a reduction system commuting with beta reduction in the partial lambda calculus
• A list-oriented extension of the lambda-calculus satisfying the Church-Rosser theorem
• Gamma-reduction in type theory of acyclic recursion
• scientific article; zbMATH DE number 1953288 (Why is no real title available?)
• Strong normalization from weak normalization in typed \(\lambda\)-calculi
• On \(\Pi\)-conversion in the \(\lambda\)-cube and the combination with abbreviations
• Reducibility Proofs in the λ-Calculus
• \(\lambda_{\beta'}\) -- a \(\lambda\)-calculus with a generalized \(\beta\)-reduction rule
• Shrinking lambda expressions in linear time
• scientific article; zbMATH DE number 4179330 (Why is no real title available?)
• Reduction graphs in the lambda calculus
• Redexes are stable in the \(\lambda\)-calculus
• scientific article; zbMATH DE number 1444323 (Why is no real title available?)
• A unified approach to type theory through a refined \(\lambda\)-calculus
• Needed reduction and spine strategies for the lambda calculus
• Generalized finite developments

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)