Refining reduction in the lambda calculus

DOI10.1017/S0956796800001507zbMath0846.68057OpenAlexW2118527795MaRDI QIDQ4880488

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)

Related Items

A unified approach to type theory through a refined \(\lambda\)-calculus ⋮ Strong normalization from weak normalization in typed \(\lambda\)-calculi ⋮ Canonical typing and ∏-conversion in the Barendregt Cube ⋮ De Bruijn's syntax and reductional behaviour of \(\lambda\)-terms: the untyped case ⋮ THE SOUNDNESS OF EXPLICIT SUBSTITUTION WITH NAMELESS VARIABLES ⋮ On \(\Pi\)-conversion in the \(\lambda\)-cube and the combination with abbreviations

Cites Work

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