Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in(…)
summary
Presents a type system that adds a freshness qualifier to reachability types so newly allocated values remain distinct until substituted, enabling precise tracking of aliasing, separation, and one-step reachability without eager transitive closure. Defines a simply-typed λ✦ and an F<:✦ with bounded reachability polymorphism, proves progress, preservation (qualifiers only grow via allocation), and preservation of separation in Coq, and ships a working prototype called the Diamond Language for experiments.
AI-written summary · about
chapters (10)
- 0:00Polymorphic reachability types intro
- 1:24Rust ownership limits
- 2:52Sharing vs functional programming
- 4:17Freshness marker for resources
- 7:30Scoped vs non-scoped resources
- 8:56Observable separation for mutation
- 11:24Reachability polymorphism
- 12:47Formalization and proofs
- 13:49Implementation and research
- 14:33Conclusion & Q&A
related talks
18mPolymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in ...
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
21mPolymorphic Type Inference for Dynamic Languages
19mExtensible Metatheory Mechanization via Family Polymorphism
17mA Better Approximation for Interleaved Dyck Reachability
14mThe Simple Essence of Monomorphization
14mDestination calculus: A linear λ-calculus for purely functional memory writes
21mPolymorphic Typestate for Session Types