Scopes as Types

on YouTube ↗27m

" summary

Scope graphs model name binding and the paper’s main claim is that treating scopes as types lets one encode structural and generic type internals uniformly. A new meta-language Statix and a committed-choice solver implement declarative rules that interleave graph construction and delayed name-resolution; specs execute for STLC with records, System F and Featherweight Generic Java. The implementation succeeds on many test suites but fails on user-written cyclic specifications where queries and edge construction depend on each other.

AI-written summary · about

" chapters (18)

1. 0:00Intro
2. 2:13Declarative Specification and Name Resolution
3. 2:47Binding: Lexical
4. 4:13Binding: Structural Records
5. 5:37Binding: Modules
6. 6:36Common Binding Representations in Specifications
7. 7:22Our Approach
8. 8:02Scope Graph: Lexical
9. 10:23Scope Graph: Records
10. 11:39Scope Graph: Modules
11. 13:28Statix: Declarative Rules
12. 16:22Interleave Graph Construction and Queries
13. 18:07Execution by Rewriting
14. 19:19Unorderable Constraints get Stuck
15. 20:30Implementation
16. 20:56Case Studies: Setup
17. 21:33Case Studies: Languages
18. 22:14Declarative, Executable Type System Specifications