Big Steps in Higher-Order Mathematical Operational Semantics
summary
Proves an abstract categorical equivalence between small‑step and big‑step for higher‑order SOS by defining a categorical big‑step SOS format and a construction from abstract higher‑order GSOS to it and back, requires a signature split into values and computations with a monotone behavior functor to support multi‑step (lists/fixpoints) and handles nondeterminism via power‑set behaviors, identifies a syntactic forbiddance captured as separated and strongly separated rules to ensure equivalence, and ships a runnable Haskell artifact with combinatory and lambda calculus examples.
AI-written summary · about
chapters (9)
- 0:00Higher-order semantics intro
- 3:31Research motivation
- 7:45Problem statement
- 10:38Abstract GSOS formalization
- 15:02Big step modeling
- 18:58Equivalence with small step
- 21:26Binders and lambda calculus
- 22:31Haskell implementation
- 24:21Q&A
related talks
24mTowards a Higher-Order Mathematical Operational Semantics
25mBig-Stop Semantics: Small-Step Semantics in a Big-Step Judgment
28mTowards Light-Weight Operational Reasoning for Languages with Binders, Categorically
27mHigher-Order Behavioural Conformances via Fibrations
15mStable Relations and Abstract Interpretation of Higher-Order Programs
02h 50mIntro to Type Systems and Operational Semantics
24mTransforming Big-Step to Small-Step Semantics Using Interpreter Specialisation
26mCombining Small-Step and Big-Step Semantics to Verify Loop Optimizations