SPLASH 2023
Sun 22 - Fri 27 October 2023 Cascais, Portugal

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 also reasoning about side effects and resource lifetimes, providing a link to two other fundamental problems.

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” in the annual Stack Overflow Developer Survey seven times in a row.

IWACO’23 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.
Plenary
You're viewing the program in a time zone which is different from your device's time zone change time zone

Tue 24 Oct

Displayed time zone: Lisbon change

09:00 - 10:30
IWACO Keynote SessionIWACO at Room XIII
Chair(s): Aleksander Boruch-Gruszecki EPFL
09:00
15m
Day opening
Welcome to IWACO!
IWACO
09:15
75m
Keynote
Capture Tracking in Scala
IWACO
10:30 - 11:00
Coffee BreakCatering at Gallery
11:00 - 12:30
IWACO Session 1IWACO at Room XIII
Chair(s): Aleksander Boruch-Gruszecki EPFL
11:00
30m
Talk
Borrow checking Hylo
IWACO
Dimi Racordon Northeastern University, USA, Dave Abrahams Adobe
File Attached
11:30
30m
Talk
Degrees of Separation: A Flexible Type System for Data Race Prevention
IWACO
File Attached
12:00
30m
Talk
Latte: Lightweight Aliasing Tracking for Java
IWACO
Conrad Zimmerman Brown University, Catarina Gamboa Carnegie Mellon University and LASIGE, University of Lisbon, Alcides Fonseca LASIGE, University of Lisbon, Jonathan Aldrich Carnegie Mellon University
Pre-print
12:30 - 14:00
14:00 - 15:30
IWACO Session 2IWACO at Room XIII
Chair(s): Aleksander Boruch-Gruszecki EPFL
14:00
30m
Talk
A Mechanized Theory of the Box Calculus
IWACO
File Attached
14:30
30m
Talk
Compositional Reasoning about Advanced Iterator Patterns in Rust
IWACO
Aurel Bílý ETH Zurich, Jonas Hansen ETH Zurich, Alexander J. Summers University of British Columbia, Peter Müller ETH Zurich
File Attached
15:00
30m
Talk
Oxidize: A Step-Debugger for Static Semantics
IWACO
Peter Chon Harvard University, Dimi Racordon Northeastern University, USA, Nada Amin Harvard University
File Attached
15:30 - 16:00
Coffee BreakCatering at Gallery

Call for Papers

We welcome submissions describing novel ideas, open questions, (preliminary) research results, or projects related to the workshop’s topics. Submitted papers can describe work-in-progress, to help foster a healthy discussion. Submissions should be up to 6 pages long, excluding references and clearly marked appendices. Submissions above the page limit will not be rejected, but the reviewers are free to ignore all content above the page limit they do not find engaging. We also encourage submissions below the page limit, for instance well-written 1- or 2-page abstracts describing an interesting idea.

Papers must be prepared in LaTeX, adhering to the ACM format available at http://sigplan.org/Resources/Author/#acmart-format using the sigplan option. The review process is single-blind: reviewers can see the submission’s authors.

Papers must be submitted via HotCRP: https://iwaco23.hotcrp.com.

Accepted submissions can be presented both in-person and remotely.