Strongly reducing variants of the Krivine abstract machine

DOI10.1007/S10990-007-9015-ZMaRDI QIDQ2464720zbMATH OpenOpenAlexFDO

Authors P. Crégut

Publication date 17 December 2007

Published in Higher-Order and Symbolic Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10990-007-9015-z

zbMATH Keywords

Abstract machinesStrong normalization

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Recommendations

• The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: a proof via corresponding calculus
• Abstract machines, optimal reduction, and streams
• scientific article; zbMATH DE number 7324353
• From outermost reduction semantics to abstract machine
• Krivine machines and higher-order schemes
• Krivine machines and higher-order schemes
• An abstract machine for the Kell calculus
• Modified strong reduction in combinatory logic
• A mechanization of strong Kleene logic for partial functions
• On the complexity-relativized strong reducibilities

Cites work

• scientific article; zbMATH DE number 1301729 (Why is no real title available?)
• scientific article; zbMATH DE number 742718 (Why is no real title available?)
• A compiled implementation of strong reduction
• Confluence properties of weak and strong calculi of explicit substitutions
• Explicit substitutions
• Functional runtime systems within the lambda-sigma calculus
• Parallel beta reduction is not elementary recursive
• The lambda calculus, its syntax and semantics

Cited in

(20)

• The useful MAM, a reasonable implementation of the strong -calculus
• Programming Languages and Systems
• scientific article; zbMATH DE number 7204429 (Why is no real title available?)
• Explaining Gabriel-Zisman localization to the computer
• (In)efficiency and reasonable cost models
• The dynamic geometry of interaction machine: a token-guided graph rewriter
• The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: a proof via corresponding calculus
• The graphical Krivine machine
• The next 700 Krivine machines
• Refunctionalization at work
• New developments in environment machines
• Equivalence of eval-readback and eval-apply big-step evaluators by structuring the lambda-calculus's strategy space
• A Fresh Look at the λ-Calculus
• Deriving an abstract machine for strong call by need
• Krivine nets: a semantic foundation for distributed execution
• A compact kernel for the calculus of inductive constructions
• IMELL cut elimination with linear overhead
• A strong distillery
• Optimizing a non-deterministic abstract machine with environments
• Improving the lazy Krivine machine

Describes a project that uses

Uses Software

• DACTL

This page was built for publication: Strongly reducing variants of the Krivine abstract machine

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