Linearity, Uniqueness, Ownership: An Entente Cordiale
This program is tentative and subject to change.
Substructural type systems, which restrict the use of weakening and contraction rules from intuitionistic logic, are growing in popularity because they allow for a resourceful interpretation of data which can be used to rule out software bugs. Substructurality is finally taking hold in practical programming: Haskell now has linear types based on Girard’s linear logic but integrated via graded function arrows, Clean has uniqueness types ensuring that values have at most a single reference, and Rust has an intricate ownership system guaranteeing memory safety. But despite this broad range of resourceful type systems, there has been comparatively little work on understanding their relative strengths and weaknesses. In our ESOP paper from 2022, we demonstrate how linear types and uniqueness types can be used within a single system in the setting of the Granule language to offer both restrictions on local program behaviour and guarantees about global memory usage. We then extend this framework further in work that will be presented later this week at OOPSLA, by showing that just like graded type systems as in Granule or Idris build upon linearity, Rust’s ownership model builds upon uniqueness. We develop an extended type system incorporating ownership and borrowing based on ideas from both fractional permissions and graded types, and implement this in Granule.
This program is tentative and subject to change.
Mon 21 OctDisplayed time zone: Pacific Time (US & Canada) change
14:00 - 15:30 | |||
14:00 30mTalk | Ordered Types for Typestate IWACO Peter Thiemann University of Freiburg, Germany | ||
14:30 30mTalk | Data-Race Safety for the Masses IWACO Holly Borla Apple, Inc, | ||
15:00 30mTalk | Linearity, Uniqueness, Ownership: An Entente Cordiale IWACO Danielle Marshall University of Glasgow |