This program is tentative and subject to change.

Mon 21 Oct 2024 15:00 - 15:30 at Pacific C - Session 3

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 Oct

Displayed time zone: Pacific Time (US & Canada) change

14:00 - 15:30
Session 3IWACO at Pacific C
14:00
30m
Talk
Ordered Types for Typestate
IWACO
Peter Thiemann University of Freiburg, Germany
14:30
30m
Talk
Data-Race Safety for the Masses
IWACO
Holly Borla Apple, Inc,
15:00
30m
Talk
Linearity, Uniqueness, Ownership: An Entente Cordiale
IWACO
Danielle Marshall University of Glasgow