On inter-deriving small-step and big-step semantics: a case study for storeless call-by-need evaluation

DOI10.1016/j.tcs.2012.02.023zbMath1244.68026OpenAlexW2151423950MaRDI QIDQ428886

Johan Munk, Kevin Millikin, Ian Zerny, Olivier Danvy

Publication date: 25 June 2012

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2012.02.023

zbMATH Keywords

continuation-passing evaluation functionheapless natural semantics for call-by-need evaluationreduction-free storeless abstract machine

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

Related Items (3)

Unnamed Item ⋮ Unnamed Item ⋮ On graph rewriting, reduction, and evaluation in the presence of cycles

Uses Software

• Coq

Cites Work

• Unnamed Item
• The lambda calculus. Its syntax and semantics. Rev. ed.
• 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
• The semantics of lazy functional languages
• Automatic autoprojection of recursive equations with global variables and abstract data types
• The revised report on the syntactic theories of sequential control and state
• Definitional interpreters revisited
• Definitional interpreters for higher-order programming languages
• Back to direct style
• A functional correspondence between call-by-need evaluators and lazy abstract machines
• Improving the lazy Krivine machine
• Continuations from generalized stack inspection
• Three Syntactic Theories for Combinatory Graph Reduction
• Lightweight fusion by fixed point promotion
• Extensional normalisation and type-directed partial evaluation for typed lambda calculus with sums
• Lazy Evaluation and Delimited Control
• Implementing lazy functional languages on stock hardware: the Spineless Tagless G-machine
• From Reduction-Based to Reduction-Free Normalization
• The call-by-need lambda calculus
• Deriving a lazy abstract machine
• The call-by-need lambda calculus
• The Zipper
• A monadic framework for delimited continuations
• The Mechanical Evaluation of Expressions
• A hybrid approach to online and offline partial evaluation
• The second Futamura projection for type-directed partial evaluation

This page was built for publication: On inter-deriving small-step and big-step semantics: a case study for storeless call-by-need evaluation