Reachability Types: Tracking Aliasing and Separation in Higher-Order Functional Programs

on YouTube ↗15m

" summary

New type system lambda assigns reachability qualifiers to expressions to track exact alias sets, enforces separation for higher-order functions with function self-qualifiers, and proves type soundness plus a preservation-of-separation theorem. An effect layer maps flow-sensitive kill effects* onto reachability sets to express move semantics, one-shot (call-once) capabilities, and safe parallel calls; this recovers nested references via move/swap. Paper includes a working prototype and a Coq mechanization of the core calculus.

AI-written summary · about

" chapters (16)

1. 0:00REACHABILITY TYPES
2. 0:10OWNERSHIP TYPE SYSTEMS
3. 1:51RETHINKING OWNERSHIP IN TERMS OF SEPARATION LOGIC
4. 2:27THE 2* CALCULUS
5. 3:51FUNCTION QUALIFIERS TRACK FREE VARIABLES
6. 5:31ESCAPING CLOSURES: HOW CAN WE TRACK THEIR FREE VARIABLES?
7. 8:04LIGHTWEIGHT REACHABILITY POLYMORPHISM
8. 8:50TYPE SOUNDNESS: PROGRESS & PRESERVATION (WRIGHT & FELLEISEN '94)
9. 9:53HIGHER-ORDER FUNCTIONS Non-Escaping Values Osvald et al 2016
10. 11:33REACHABILITY-AND-EFFECT SYSTEMS
11. 12:03FLOW-INSENSITIVE EFFECTS
12. 12:28FLOW-SENSITIVE KILL EFFECTS: ENABLE UNIQUENESS, LINEARITY, OWNERSHIP TRANSFER & MORE
13. 13:00RECOVERING NESTED REFERENCES: MOVE SEMANTICS AND OWNERSHIP TRANSFER VIA KILL EFFECTS
14. 13:24CASE STUDIES IN THE PAPER
15. 13:38EFFECT QUANTALES
16. 14:09SUMMARY & CONTRIBUTIONS