Knowing When to Ask: Sound Scheduling of Name Resolution in Type Checkers Derived from Declarative S
summary
Derives executable type checkers from Statix specifications by giving an operational semantics that schedules name resolution to avoid unstable queries; implements it as MiniStatix in Haskell, uses over-approximation of critical edges plus a scope-ownership type system to decide when to delay queries, and proves soundness and confluence of the generated checkers. Evaluation runs Java and Scala specifications against their test suites and passes them, showing the approach handles real-world name binding patterns and that the scheduler is precise enough in practice.
AI-written summary · about
chapters (5)
- 0:00Start
- 8:43Why Statis?
- 9:55The Goal
- 10:48The Scheduling Problem for Statix
- 12:38Critical Edges: a Reasoning Tool
related talks
25mIncremental Type-Checking for Free: Using Scope Graphs to Derive Incremental Type-Checkers
32mA Monadic Framework for Name Resolution in Multi-Phased Type Checkers
18mDeveloping a Dependently Typed Language with Runtime Proof Search
15mLanguage-Parametric Reference Synthesis
24mScoped and Typed Staging by Evaluation
41mThe Dialectics of Type-Level Programming
46mThe Calculated Typer (Functional Pearl)
24mDecoupling Resolution from Type Inference