Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for(…)

on YouTube ↗18m

" summary

Presents an algorithmic design for reachability types that proves sound and decidable bidirectional typing and avoidance, mechanized in Lean 4 and accompanied by reusable artifacts. It refines subtyping to allow covariant/contravariant self-references so escaping structures (including Church-encoded pairs and lists) avoid term-level coercions. The implementation infers qualifiers via lightweight unification, scales roughly quadratically, and reports under 20% annotations on evaluated examples while preserving semantic soundness.

AI-written summary · about

" chapters (11)

1. 0:00Reachability types introduction
2. 1:04Tracking resource sharing
3. 2:26Designing reachability types
4. 3:51Avoidance in dependent types
5. 5:38Self-references for escaping
6. 7:22Algorithmic sound avoidance
7. 9:06Polymorphism and bidirectional typing
8. 11:16Mechanized formalization in Lean 4
9. 12:21System evaluation and performance
10. 13:49Summary of expressive reachability
11. 14:52Q&A on annotations and evaluation