Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs

Explore a groundbreaking 18-minute video presentation from POPL 2024 that introduces polymorphic reachability types for tracking freshness, aliasing, and separation in higher-order generic programs. Delve into the challenges of adapting Rust-like substructural features to higher-level languages with functional and type-level abstraction. Learn about the new freshness qualifier and how it enables precise, sound, and parametric combination of reachability and type polymorphism. Discover the simply-typed λ✦-calculus and F✦-calculus, which offer lightweight reachability polymorphism and bounded parametric polymorphism over types and reachability qualifiers. Gain insights into potential applications for safe capability programming and effect system extensions, and compare this innovative system with Scala's capture types.