Handling Scope Checks: A Comparative Framework for Dynamic Scope Extrusion Checks
summary
Compares three concrete dynamic checks—lazy vs eager and a new Cause-for-Concern (C4C) check—and gives a formal calculus for evaluating them with effect handlers; proves C4C correct, characterises it independently of implementation, and shows it avoids eager false positives caused by resuming continuations by using a checkm that erases itself when continuations remain. Implements C4C in MetaOCaml, reports empirical validation, and notes one remaining class of false positives when malformed code is later discarded.
AI-written summary · about
chapters (9)
- 0:00Scope extrusion checks intro
- 2:27Macrochamel style meta programming
- 10:33Scope extrusion with effects
- 13:43Lazy vs eager dynamic checks
- 16:48Effect handlers and scope extrusion
- 18:33Cause for concern check
- 20:58Summary and contributions
- 21:36Q&A: Compile vs runtime meta
- 22:40Q&A: Effects in meta vs object
related talks
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
30mEffects,capabilities,and boxes: from scope-based reasoning to type-based reasoning and back
12mCompiling Effect Handlers in Capability-Passing Style
15mEffect Handlers, Evidently
15mCompiling with Continuations, Correctly
22mHigher-Order Model Checking of Effect-Handling Programs with Answer-Type Modification
01h 05mControl Flow Obfuscation for Featherweight Java + Efficient Fair Conjunction
25mIncremental Type-Checking for Free: Using Scope Graphs to Derive Incremental Type-Checkers