From Reduction-Based to Reduction-Free Normalization

DOI10.1007/978-3-642-04652-0_3zbMath1263.68036OpenAlexW398758961MaRDI QIDQ3649133

Olivier Danvy

Publication date: 3 December 2009

Published in: Advanced Functional Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-04652-0_3

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items

From Outermost Reduction Semantics to Abstract Machine ⋮ Generating Specialized Interpreters for Modular Structural Operational Semantics ⋮ Isomorphic Interpreters from Logically Reversible Abstract Machines ⋮ A functional approach to generic programming using adaptive traversals ⋮ On inter-deriving small-step and big-step semantics: a case study for storeless call-by-need evaluation ⋮ Three Syntactic Theories for Combinatory Graph Reduction ⋮ On graph rewriting, reduction, and evaluation in the presence of cycles ⋮ Inter-deriving semantic artifacts for object-oriented programming ⋮ The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus ⋮ A correspondence between type checking via reduction and type checking via evaluation

Uses Software

• ML

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• An abstract framework for environment machines
• A syntactic correspondence between context-sensitive calculi and abstract machines
• Refunctionalization at work
• On the equivalence between small-step and big-step abstract machines: a simple application of lightweight fusion
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Definitional interpreters revisited
• Back to direct style
• From syntactic theories to interpreters: Automating the proof of unique decomposition
• The origins of structural operational semantics
• A structural approach to operational semantics
• A functional correspondence between call-by-need evaluators and lazy abstract machines
• A functional correspondence between monadic evaluators and abstract machines for languages with computational effects
• Trampolined style
• Lightweight fusion by fixed point promotion
• Recursive functions of symbolic expressions and their computation by machine, Part I
• Inter-deriving Semantic Artifacts for Object-Oriented Programming
• The Theory of Calculi with Explicit Substitutions Revisited
• A Rational Deconstruction of Landin's SECD Machine with the J Operator
• Functional runtime systems within the lambda-sigma calculus
• Representing Control: a Study of the CPS Transformation
• Thunks and the λ-calculus
• The Zipper
• A concrete framework for environment machines
• An Operational Foundation for Delimited Continuations in the CPS Hierarchy
• A Rational Deconstruction of Landin’s SECD Machine
• On one-pass CPS transformations
• Making a fast curry: push/enter vs. eval/apply for higher-order languages
• Logic Based Program Synthesis and Transformation
• The Mechanical Evaluation of Expressions
• Binding-time analysis for both static and dynamic expressions