An Incremental Approach to the Semantics of Borrowing
This program is tentative and subject to change.
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.
This program is tentative and subject to change.
Mon 2 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
11:00 - 12:30 | |||
11:00 30mTalk | Amplifying Contextual Distance in Higher-Order Languages, using the Law of Large Numbers HOPE | ||
11:30 30mTalk | An Incremental Approach to the Semantics of Borrowing HOPE Brianna Marshall Northeastern University, Andrew Wagner Northeastern University, John Li Northeastern University, Olek Gierczak Northeastern University, Amal Ahmed Northeastern University, USA | ||
12:00 30mTalk | Towards a linear functional translation for borrowing HOPE |