Strongly reducing variants of the Krivine abstract machine

DOI10.1007/S10990-007-9015-ZzbMATH Open1130.68052OpenAlexW2031190840MaRDI QIDQ2464720FDOQ2464720

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

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

zbMATH Keywords

Abstract machinesStrong normalization

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Cites Work

• The lambda calculus, its syntax and semantics
• Explicit substitutions
• Parallel beta reduction is not elementary recursive
• A compiled implementation of strong reduction
• Functional runtime systems within the lambda-sigma calculus
• Confluence properties of weak and strong calculi of explicit substitutions
• Title not available (Why is that?)
• Title not available (Why is that?)

Cited In (17)

• Title not available (Why is that?)
• Title not available (Why is that?)
• 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
• (In)efficiency and reasonable cost models
• Explaining Gabriel-Zisman localization to the computer
• The graphical Krivine machine
• The next 700 Krivine machines
• Refunctionalization at work
• New developments in environment machines
• A Fresh Look at the λ-Calculus
• Krivine nets: a semantic foundation for distributed execution
• A strong distillery
• A compact kernel for the calculus of inductive constructions
• Improving the lazy Krivine machine
• Programming Languages and Systems
• The useful MAM, a reasonable implementation of the strong \(\lambda\)-calculus

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)