Algebraic Stepper for Simple Modules
summary
An OCaml algebraic stepper is implemented for simple hierarchical modules (no functors or signature sealing) that shows execution by delayed substitution of variables and by attaching level-annotated variables to maintain correct module references. Formalized semantics prove consistency with standard small‑step semantics after an erasure step. The stepper supports recursion, records, lists, exceptions, is used in an introductory OCaml course, and currently exposes module internals rather than honoring sealing.
AI-written summary · about
chapters (7)
- 0:00Algebraic stepper intro
- 2:10Algebraic stepper vs small-step
- 8:48Modules in algebraic stepper
- 14:55Formalizing the stepper
- 20:01Related work on stepping
- 21:51Current status and plans
- 23:18Q&A
related talks
01h 35mRecursion Schemes, Algebras, Finally Tagless, Data Types
46mFinite-state machines? Your compiler wants in!
01h 44mPractical Observable Sharing
01h 37mThe Art of Program Derivation and Parallel Computation
46mFrom Chaos to Cohesion: Building Modular Monoliths in the Real World
36mData Driven UIs, Incrementally
08mReason and OCaml - The Full Stack
01h 04mWhat FP Can Learn From Formal Languages: Towards a Leaner Syntax