A natural semantics for lazy evaluation

1993/01/01 by John Launchbury · 10 citations
Computer Science · #Logic, programming, and type systems #Logic, Reasoning, and Knowledge #Advanced Database Systems and Queries

paper · doi:10.1145/158511.158618

openalex publication_date 1993/01/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/29

Abstract

We define an operational semantics for lazy evaluation which provides an accurate model for sharing. The only computational structure we introduce is a set of bindings which corresponds closely to a heap. The semantics is set at a considerably higher level of abstraction than operational semantics for particular abstract machines, so is more suitable for a variety of proofs. Furthermore, because a heap is explicitly modelled, the semantics provides a suitable framework for studies about space behaviour of terms under lazy evaluation.

Cited by

• Sequent calculus as a compiler intermediate language
• Demonstrating Lambda Calculus Reduction
• Uniform confluence in concurrent computation
• Functional computation as concurrent computation
• Singular and plural functions for functional logic programming
• Reasoning about the garden of forking paths
• Effectful Programming in Declarative Languages with an Emphasis on\n Non-Determinism: Applications and Formal Reasoning
• A practical mode system for recursive definitions
• Small-step and big-step semantics for call-by-need
• Lazy evaluation [wikipedia]