Writing

1. Explicit substitutions in lambda calculus

   Making substitution steps explicit and lifting pending substitutions under binders without capturing free variables

2. Proof obligations for jump threading and block merging

   The side conditions under which jump threading and block merging preserve behaviour, the simulation relations that discharge them, and a validator that checks duplicated control flow against its source.

3. Bayesian model merging for stochastic context-free grammar induction

   Inducing stochastic context free grammars from samples, after Stolcke and Omohundro

4. Reverse engineering the R4 DEMON expiry check

   Tracing the R4 kernel expiry check through ARM9 startup and repairing the integrity metadata required to keep the patched menu running

5. Continuation ownership and cancellation under algebraic effects

   How cancellation requests reach suspended computations and how continuation ownership, backend registrations and scope lifetimes determine whether cleanup actually finishes

6. Ranked tree pattern matching with path automata

   Recognising tree patterns through shared paths and automaton states, with an interactive demo for trying patterns against nested subjects