Capabilities, Effects, Ownership, and Behaviors
Ownership types and effects have long been recognized as related, with ownership types proposed to tame the side effects in large programs by restricting either access or mutation of an object to its owning object’s code. Capabilities are now recognized to serve a similar role, with many ownership systems being cast as (reference) capability systems. But all ownership systems, and most capability systems, are limited to asking or checking whether code does or does not modify particular objects or resources, which despite it’s limits serves the original goals of training about where changes do (not) occur.
Capability systems that go beyond this trend to stick to a fixed set of possible changes, and whether each may or may not occur. Order of changes is rarely considered, despite the value in knowing that certain orders of updates may preserve or violate properties of interest, or even crash a program. Recent years have seen interest in formalizing the relationship between capability systems and effect systems (another family of static techniques) through the view that the input capabilities provided to code determine an upper bound on its effect. But while effect systems have evolved to address ordering of changes, few capability systems have.
We will discuss extending and refining the relationship between capabilities and effects to deal with ordering of events over time, and what it means to extend that relationship back to ownership systems — what does it mean for an owner to specify not only the footprint of its representation, but how it uses its representation over time?
Mon 21 OctDisplayed time zone: Pacific Time (US & Canada) change
11:00 - 12:30 | |||
11:00 30mTalk | Capabilities, Effects, Ownership, and Behaviors IWACO Colin Gordon Drexel University | ||
11:30 30mTalk | Modular Borrowing Without Ownership or Linear Types IWACO Lionel Parreaux HKUST (The Hong Kong University of Science and Technology) Media Attached File Attached | ||
12:00 30mTalk | Substructural Information Flow via Polymorphism IWACO Hemant Gouni Carnegie Mellon University, Pittsburgh, Pennsylvania, United States, Jonathan Aldrich Carnegie Mellon University Media Attached File Attached |