Capabilities, Effects, Ownership, and Behaviors
summary
Argues that capability systems must track ordering by relating a flow-sensitive static capability system to a sequential effect system whose effects are program traces; proves a mapping where capabilities capability bounding upper‑bound effects while effects lower‑bound capability pairs (input→output), enabling reasoning about creation, consumption, cyclic capabilities and residuals. Implements these ideas against real-language features (exceptions, continuations) and shows the pairwise capability view forms an effect quantale, which yields new behavioral ownership notions (owner-as-dominator, owner-for-critical-ops) for preserving invariants over time.
AI-written summary · about
chapters (5)
- 0:00Introduction
- 2:29Static reasoning systems
- 7:30Capability bounding vs effects
- 15:30Behaviors and capabilities
- 24:39Future directions
related talks
36mObject Capabilities
24mImplementing a Capability Machine Model into Iris
29mEfficient, Provable Local Capability Revocation using Uninitialized Capabilities
23mSecurity Reasoning via Substructural Dependency Tracking
19mGradient: Gradual Compartmentalization via Object Capabilities Tracked in Types
17mProving capability safety in the presence of indirect sentries
27mLe Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed
40mEnvironmental Dependencies as Coeffects