Linear type systems are useful for managing ownership of resources, but they can be cumbersome to use: resources passed temporarily to a function must be explicitly threaded through and returned. Rust offers flexibility by allowing a resource to be borrowed before passing it to a function, so the original owner automatically gets it back when the lifetime of the borrow ends.

In this work, we elucidate the semantics of borrowing, by starting with a linear language with only support for ownership or resources, and gradually adding immutable borrows, lifetimes, mutable borrows, and finally lifetime polymorphism. We present a semantic model, a domain-specific separation logic, and a type system for each stage of our borrowing system, and prove semantic type soundness of each using the logics. As a corollary of our semantic soundness result, we have that each of the calculi are terminating and do not leak memory. We also show that our separation logic can be used to reason beyond typed programs and validate programs that safely break and reestablish invariants.