Strongly reducing variants of the Krivine abstract machine

DOI10.1007/s10990-007-9015-zzbMath1130.68052OpenAlexW2031190840MaRDI QIDQ2464720

Pierre 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)

Related Items

Explaining Gabriel-Zisman localization to the computer ⋮ Unnamed Item ⋮ Refunctionalization at work ⋮ Unnamed Item ⋮ Unnamed Item ⋮ The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus ⋮ The Useful MAM, a Reasonable Implementation of the Strong $$\lambda $$ -Calculus ⋮ A Fresh Look at the λ-Calculus ⋮ A compact kernel for the calculus of inductive constructions ⋮ (In)efficiency and reasonable cost models

Uses Software

• DACTL

Cites Work

• Unnamed Item
• Unnamed Item
• The lambda calculus, its syntax and semantics
• 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
• Explicit substitutions