Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs
ACM SIGPLAN via YouTube
Our career paths help you become job ready faster
AI Engineer - Learn how to integrate AI into software applications
Overview
Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
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.
Syllabus
[POPL'24] Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in ...
Taught by
ACM SIGPLAN