Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment
summary
Extends big-step semantics with a nondeterministic big-stop rule schema that captures every finite prefix of diverging small-step runs, proving equivalence to the reflexive‑transitive closure of small-step reduction. Applies to typed, untyped, and effectful PCF, and verifies compilation to a K machine (including effects). Mechanized Agda proofs and artifacts available; the big-stop formalization is substantially smaller than a small-step development (authors report small-step encodings are about twice as big) and can be optimized to a single-rule big-stop form.
AI-written summary · about
chapters (8)
- 0:00Big-stop semantics intro
- 2:09Big-step limits
- 5:20Ideal semantics wish list
- 8:31Non-termination inductive approaches
- 12:19Big-stop core idea
- 16:13Advantages over small-step
- 17:38PCF to K machine case study
- 21:34Q&A
related talks
24mTransforming Big-Step to Small-Step Semantics Using Interpreter Specialisation
26mCombining Small-Step and Big-Step Semantics to Verify Loop Optimizations
27mBig Steps in Higher-Order Mathematical Operational Semantics
24mA Big-Step Compositional Continuation-Passing Semantics for WebAssembly
24mA Computational Interpretation of Compact Closed Categories
28mCombinator-Based Fixpoint Algorithms for Big-Step Abstract Interpreters
18mDeferring the Details and Deriving Programs
15mCompiling with Continuations, Correctly