A functional correspondence between call-by-need evaluators and lazy abstract machines

DOI10.1016/j.ipl.2004.02.012zbMath1178.68249OpenAlexW1966776129MaRDI QIDQ2390256

Jan Midtgaard, Olivier Danvy, Mads Sig Ager

Publication date: 21 July 2009

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ipl.2004.02.012

zbMATH Keywords

functional programmingprogram derivationabstract machinesdefunctionalizationinterpretersCPS transformationclosure conversion

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (19)

Systematic abstraction of abstract machines ⋮ Cutting Out Continuations ⋮ Proofs, Upside Down ⋮ A syntactic correspondence between context-sensitive calculi and abstract machines ⋮ Calculating Certified Compilers for Non-deterministic Languages ⋮ Normalization by evaluation for modal dependent type theory ⋮ Programming language semantics: It’s easy as 1,2,3 ⋮ Automating the functional correspondence between higher-order evaluators and abstract machines ⋮ Inter-deriving Semantic Artifacts for Object-Oriented Programming ⋮ On inter-deriving small-step and big-step semantics: a case study for storeless call-by-need evaluation ⋮ Calculating correct compilers ⋮ Refunctionalization at work ⋮ Improving the lazy Krivine machine ⋮ A static simulation of dynamic delimited control ⋮ Inter-deriving semantic artifacts for object-oriented programming ⋮ Unnamed Item ⋮ Unnamed Item ⋮ From Reduction-Based to Reduction-Free Normalization ⋮ A functional correspondence between monadic evaluators and abstract machines for languages with computational effects

Uses Software

• ALGOL 60

Cites Work

• The semantics of lazy functional languages
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Definitional interpreters for higher-order programming languages
• Improving the lazy Krivine machine
• A functional correspondence between monadic evaluators and abstract machines for languages with computational effects
• Functional runtime systems within the lambda-sigma calculus
• From operational semantics to abstract machines
• Deriving a lazy abstract machine
• A Rational Deconstruction of Landin’s SECD Machine
• The Mechanical Evaluation of Expressions
• On the transformation between direct and continuation semantics
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A functional correspondence between call-by-need evaluators and lazy abstract machines