An Incremental Approach to the Semantics of Borrowing
summary
Presents a core, extensible borrow calculus built incrementally: start from a linear call-by-push-value core, add immutable borrows, lifetimes, mutable borrows, and lifetime polymorphism; produce a type system and a domain-specific separation logic for each stage and prove semantic type soundness (semantic model proof is in progress). Claims the calculi terminate and enforce no use-after-free, exclusive-or-immutability aliasing, and no memory leaks; excludes non-lexical lifetimes and does not yet provide a mechanized formalization.
AI-written summary · about
chapters (11)
- 0:00Borrowing in Rust
- 1:25Borrowing prevents memory issues
- 3:54Borrowing research challenges
- 7:12Borrow Zoo features
- 10:26Core borrowing calculus
- 12:54Downward-only borrowing
- 14:39Extending the type system with lifetimes
- 20:01Mutable borrows
- 21:44Separation logic for borrowing
- 23:51Future directions
- 25:42Q&A
related talks
19mPure Borrow: Linear Haskell Meets Rust-Style Borrowing
40mAgainst Borrowing: Own the forest, not the trees!
32mThe First Six Years in the Development of Polonius, an Improved Borrow Checker
26mThe first six years in the development of Polonius
53mThe Rust Borrow Checker - A Deep Dive
36mThe Rust Borrow Checker: A Deep Dive
50mRust's Borrow Checker Proven Correct!
35mPolonius: Either Borrower or Lender Be, but Responsibly