Ownership and capability systems have emerged, independently and across a wide range of ecosystems, as a unifying way to govern aliasing, access, effect boundaries, and resource lifetimes. Ownership controls what references to a resource may exist and who may use them; capabilities control what code may do with the resources it can reach. Together they turn assumptions that used to live in comments, folklore, and review discipline into properties a compiler, runtime, verifier, or processor can check. They now appear in statically and dynamically typed languages, in functional and imperative ones, in managed runtimes and in silicon, and in verification tools that exploit ownership structure to cut proof burden. These systems have demonstrated benefits including race-free concurrency, memory-safe resource usage, predictable performance, and easier verification.

What has not emerged is a shared understanding of why they work. Many of these communities face analogous challenges under different constraints, design pressures, and implementation levers: how to transfer an object graph safely between threads, where to place the boundary between checked and unchecked code, how to retrofit a discipline onto code that predates it. Each has answered in its own vocabulary. Ownership, capabilities, effects, isolation, and aliasing control all recur across ecosystems with subtly different meanings; as reported in the 2023 POPL tutorial RUST: Regions, Uniqueness, Ownership & Types, whole research traditions have independently rediscovered much the same ideas without recognizing the overlap. The same fragmentation separates static from dynamic languages, managed runtimes from systems languages, and software enforcement from hardware. This Dagstuhl Seminar exists to close gaps such as these: to compare application experience across contexts that impose genuinely different pragmatics, and to work out which divergences are essential and which are accidental.

The seminar will explore five broad themes.

Verification is a cross-cutting concern throughout these themes: it can establish safety properties, reduce proof burden and state-space explosion, and clarify the guarantees provided by different enforcement points and substructural foundations.

1. Concurrency safety. How ownership and capabilities can eliminate data races by ruling out unsynchronized mutation, and how they fare inside concurrency models as different as threads, actors, tasks, and message passing. What alias and capture discipline does safe parallelism actually require, and how much of it can be checked at compile time?
2. Memory safety. How regions, affine ownership, and capability-tracked lifetimes prevent spatial and temporal errors, and how ownership information can be exploited for efficient and/or predictable memory management — including hybrid schemes that mix manual reclamation with collection. What lifetime discipline do resource APIs need, and how do region and borrowing models interact with a collector?
3. Retrofitting and integration. Most software in production predates these ideas entirely, and clean-room rewriting does not scale. What strategies, tooling, and annotation burdens make incremental adoption viable in an existing language or library, and what do experience reports from real retrofits tell us about where the boundaries between checked and unchecked code should fall?
4. Enforcement points. Checks can live in the type system, the compiler, the runtime, the hardware, or the verifier, and the choice changes what can be guaranteed and what it costs. Where is ownership metadata worth exploiting to remove redundant synchronization or memory barriers, how do capability architectures shift the trade-off, and how does ownership structure reduce state-space explosion and proof burden?
5. Substructural foundations and shared terminology. Linearity, affinity, uniqueness, separation, and permission logics all explain parts of why the practical systems are sound. What are the minimal foundations needed to justify the rules that shipping languages actually enforce, where do the underlying logics genuinely diverge across paradigms, and can we agree on a vocabulary precise enough to make the comparison possible?

Our aim is synthesis rather than the presentation of results: a shared terminology, a lightweight taxonomy of the design space that exposes recurring patterns and real divergences, and an application-oriented roadmap identifying where joint progress across these communities is most achievable.

Creative Commons BY 4.0

Mae Milano, Peter Müller, Matthew Parkinson, and Tobias Wrigstad