Needed reduction and spine strategies for the lambda calculus

DOI10.1016/0890-5401(87)90001-0zbMATH Open0635.03009OpenAlexW2147478629MaRDI QIDQ1097253FDOQ1097253

Authors: Henk Barendregt, J. R. Kennaway, M. R. Sleep, Jan Willem Klop 

Publication date: 1987

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://ir.cwi.nl/pub/1726

Recommendations

• Refining reduction in the lambda calculus
• scientific article; zbMATH DE number 1547348
• Term Rewriting and Applications
• Reducibility Proofs in the λ-Calculus
• Parallel reductions in \(\lambda\)-calculus
• Parallel reductions in \(\lambda\)-calculus
• Reduction graphs in the lambda calculus
• The self-reduction in lambda calculus
• scientific article; zbMATH DE number 7084951
• Combinatory weak reduction in lambda calculus

zbMATH Keywords

programming languagesreduction to normal formneeded redexspine redexes

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Combinatory logic and lambda calculus (03B40)

Cites Work

• Title not available (Why is that?)
• Edinburgh LCF. A mechanized logic of computation
• Title not available (Why is that?)
• The Mechanical Evaluation of Expressions
• Title not available (Why is that?)
• The next 700 programming languages
• Minimal and Optimal Computations of Recursive Programs
• A new implementation technique for applicative languages
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Sequential evaluation strategies for parallel-or and related reduction systems
• Strictness analysis for higher-order functions
• Title not available (Why is that?)

Cited In (16)

• Minimal relative normalization in orthogonal expression reduction systems
• The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: a proof via corresponding calculus
• A unified approach to type theory through a refined \(\lambda\)-calculus
• Strictness analysis via abstract interpretation for recursively defined types
• Perpetual reductions in \(\lambda\)-calculus
• A Logical Interpretation of the λ-Calculus into the π-Calculus, Preserving Spine Reduction and Types
• Title not available (Why is that?)
• Sequentiality in orthogonal term rewriting systems
• A safe approach to parallel combinator reduction
• Highlights in infinitary rewriting and lambda calculus
• Making ``stricterness more relevant
• Refining reduction in the lambda calculus
• Title not available (Why is that?)
• Formal verifications of call-by-need and call-by-name evaluations with mutual recursion
• Descendants and origins in term rewriting.
• Relative normalization in Deterministic Residual Structures

Uses Software

• Miranda

This page was built for publication: Needed reduction and spine strategies for the lambda calculus

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