Incremental Bidirectional Typing via Order Maintenance
summary
Presents a small-step incremental bidirectional type system that maintains binding pointers with an order maintenance data structure so inserts/deletes and comparisons are amortized O(1) and ancestor checks reduce to interval comparisons; lowest-binder lookup is polylog by per-name balanced trees. Mechanized equivalence and metatheory via Agda mechanization. Provides an optimized OCaml implementation and a large stress test showing multiple orders-of-magnitude speedup versus from-scratch reanalysis; artifacts and reproductions available.
AI-written summary · about
chapters (8)
- 0:00Introduction
- 1:50Live programming at scale
- 3:16Incremental type checking
- 4:41Formal guarantees
- 6:05Update order challenges
- 8:13Order maintenance structure
- 11:22Comparison with prior work
- 12:45Q&A
related talks
34mIncremental Bidirectional Typing via Order Maintenance
25mIncremental Type-Checking for Free: Using Scope Graphs to Derive Incremental Type-Checkers
21mGrove: A Bidirectionally Typed Collaborative Structure Editor Calculus
38mType System Foundations for Super-Charged Semantic Code Search
27mGradual Typing in Practice
01h 06mOn-The-Fly Verification via Incremental, Interactive Abstract Interpretation wi...
01h 00mA Type-Safe Structure Editor Calculus + Strictly Capturing Non-Strict Closures
18mIntroducing the Bindoj library, a datatype-centric generative programming libr...