PLDI 2025
Mon 16 - Fri 20 June 2025 Seoul, South Korea

This program is tentative and subject to change.

Thu 19 Jun 2025 14:00 - 14:20 at Cosmos, Violet & Tulip - Language Design

The Rust programming language is well known for its ownership-based type system, which offers strong guarantees like memory safety and data race freedom. However, Rust also provides unsafe escape hatches, for which safety is not guaranteed automatically and must instead be manually upheld by the programmer. This creates a tension. On the one hand, compilers would like to exploit the strong guarantees of the type system—particularly those pertaining to aliasing of pointers—in order to unlock powerful intraprocedural optimizations. On the other hand, those optimizations are easily invalidated by “badly behaved” unsafe code. To ensure correctness of such optimizations, it thus becomes necessary to clearly define what unsafe code is “badly behaved.” In prior work, Stacked Borrows defined a set of rules achieving this goal. However, Stacked Borrows rules out several patterns that turn out to be common in real-world unsafe Rust code, and it does not account for advanced features of the Rust borrow checker that were introduced more recently.

To resolve these issues, we present Tree Borrows. As the name suggests, Tree Borrows is defined by replacing the stack at the heart of Stacked Borrows with a tree. This overcomes the aforementioned limitations: our evaluation on the 30 000 most widely used Rust crates shows that Tree Borrows rejects 54% fewer test cases than Stacked Borrows does. Additionally, we prove (in Rocq) that it retains most of the Stacked Borrows optimizations and also enables important new ones, notably read-read reorderings.

This program is tentative and subject to change.

Thu 19 Jun

Displayed time zone: Seoul change

14:00 - 15:00
14:00
20m
Talk
Tree Borrows
PLDI Research Papers
Neven Villani University of Grenoble Alpes - VERIMAG, Johannes Hostert ETH Zurich, Derek Dreyer MPI-SWS, Ralf Jung ETH Zurich
Link to publication DOI
14:20
20m
Talk
Principal Type Inference under a Prefix: A Fresh Look at Static Overloading
PLDI Research Papers
Daan Leijen Microsoft Research, Wenjia Ye National University of Singapore; University of Hong Kong
DOI Pre-print
14:40
20m
Talk
Efficient, Portable, Census-Polymorphic Choreographic Programming
PLDI Research Papers
Mako P. Bates University of Vermont, Shun Kashiwa University of California at San Diego, Syed Jafri University of Vermont, Gan Shen University of California at Santa Cruz, Lindsey Kuper University of California at Santa Cruz, Joseph P. Near University of Vermont
DOI Pre-print