Transforming Big-Step to Small-Step Semantics Using Interpreter Specialisation
summary
Transforms big-step semantics into small-step rules by writing the big-step rules as Horn clauses and encoding an interpreter specialization that executes big-step rules in small steps. The implementation uses a partial evaluator (Loogen) to specialize the interpreter and produces line-for-line small-step Horn clauses for examples such as miniML. The generated small-step semantics run and match the original big-step runs on tests, but no formal correctness proof yet; next target is Blazy and Leroy’s CompCert-like C semantics.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 0:29Motivation and research
- 1:32Big-step vs small-step
- 5:25Semantics as Horn clauses
- 6:48Interpreter specialization
- 8:35Big-step to small-step
- 12:10Interpreter design
- 14:22Demo: mini ML semantics
- 16:54Validation and future work
- 17:57Certified C compiler
- 19:23Correctness proof
- 21:32Q&A
related talks
25mBig-Stop Semantics: Small-Step Semantics in a Big-Step Judgment
26mCombining Small-Step and Big-Step Semantics to Verify Loop Optimizations
21mSynthesizing Formal Semantics from Executable Interpreters
27mBig Steps in Higher-Order Mathematical Operational Semantics
35mDeriving an Erlang Interpreter from a Mechanised Formal Semantics of Core Erlang
30mSemantics-Guided Synthesis
24mA Big-Step Compositional Continuation-Passing Semantics for WebAssembly
28mCombinator-Based Fixpoint Algorithms for Big-Step Abstract Interpreters