From Reduction-Based to Reduction-Free Normalization
From MaRDI portal
Publication:3649133
DOI10.1007/978-3-642-04652-0_3zbMath1263.68036OpenAlexW398758961MaRDI QIDQ3649133
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
Related Items (10)
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
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
This page was built for publication: From Reduction-Based to Reduction-Free Normalization
