Basic Mechanics of Operational Semantics
summary
Crash course in reading operational rules: shows concrete syntax for a tiny arithmetic language, how to read inference rules and BNF, how big-step (natural) semantics maps expressions to integers and why it hides nontermination, how small-step (SOS) semantics exposes single-step and star closures, how to compress proofs with evaluation contexts, and how to turn semantics into an executable evaluator or an abstract machines stack machine. Illustrates relating big-step = small-step* and using machines to prove an asymptotic speedup for effect handlers.
AI-written summary · about
chapters (17)
- 0:00Intro
- 0:19Basic Mechanics of Operational Semantics
- 2:07What is an operational
- 4:47From Derek's talk
- 8:49Syntax of A
- 11:09Inference rules
- 12:49Natural semantics of A
- 17:00Evaluator semantics of A
- 19:05SOS semantics of A
- 22:16Proof of each step
- 22:36Different steps
- 26:34Reduction axioms
- 29:05Standard reductions
- 31:30Abstract (stack) machine
- 34:27Functions
- 34:39Substitution
- 36:04Exceptions