Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in ...
summary
Introduces a new freshness qualifier (diamond) that marks allocations whose reachability may materialize later, and designs two calculi (λ✦ and F✦ calculi) that combine precise reachability tracking with lightweight and bounded parametric polymorphism. Proves type soundness and a preservation-of-separation theorem, mechanizes proofs in Coq mechanization, and ships a prototype implementation called the Diamond Language. Shows that reachability sets only grow via allocation and that separation is preserved during evaluation.
AI-written summary · about
chapters (12)
- 0:00Polymorphic reachability types
- 1:45Resource tracking challenges
- 4:14Freshness markers
- 8:28Separation guarantees
- 11:19Lightweight polymorphism
- 12:22Formalization and proofs
- 13:04Conclusion and future work
- 13:46Q&A: Freshness vs nominal
- 14:29Q&A: Immutable borrowing
- 15:11Q&A: Equational theory
- 16:15Q&A: Logical relations
- 17:19Q&A: Mutually recursive typing
related talks
19mPolymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in(…)
17mA Better Approximation for Interleaved Dyck Reachability
26mProperty-Directed Reachability as Abstract Interpretation in the Monotone Theory
18mQualifying System F-sub
14mPathological Cases for a Class of Reachability-Based Garbage Collectors
15mLiberating Merges via Apartness and Guarded Subtyping
14mDestination calculus: A linear λ-calculus for purely functional memory writes
19mExtensible Metatheory Mechanization via Family Polymorphism