Needed reduction and spine strategies for the lambda calculus

DOI10.1016/0890-5401(87)90001-0MaRDI QIDQ1097253zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

• scientific article; zbMATH DE number 3646849 (Why is no real title available?)
• scientific article; zbMATH DE number 3875232 (Why is no real title available?)
• scientific article; zbMATH DE number 3951980 (Why is no real title available?)
• scientific article; zbMATH DE number 4043233 (Why is no real title available?)
• scientific article; zbMATH DE number 3695144 (Why is no real title available?)
• scientific article; zbMATH DE number 3730111 (Why is no real title available?)
• scientific article; zbMATH DE number 3735770 (Why is no real title available?)
• scientific article; zbMATH DE number 3523519 (Why is no real title available?)
• A new implementation technique for applicative languages
• Edinburgh LCF. A mechanized logic of computation
• Minimal and Optimal Computations of Recursive Programs
• Sequential evaluation strategies for parallel-or and related reduction systems
• Strictness analysis for higher-order functions
• The Mechanical Evaluation of Expressions
• The next 700 programming languages

Cited in

(16)

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

Describes a project that uses

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)