IWACO 2024
who it's for
programming language researchers, language implementers, compiler engineers, Rust developers, language tooling engineers, smart contract engineers
topics
Polonius borrow checker redesign; MIR-driven ownership visualization; linearity and uniqueness in Granule; ordered types for typestate; region-based data-race safety (Swift actors); substructural information flow via polymorphism; type-and-effect temporary borrowing; capability-sequential effect mapping; offer-safe object-capability trading (Zoe); fractional-permissions for destructive updates
| title | author | length |
|---|---|---|
| Linearity, Uniqueness, Ownership: An Entente Cordiale | Danielle Marshall | 32m |
Claims that linearity and uniqueness serve different temporal guarantees—linearity restricts the future, uniqueness guarantees the past—and that both plus… | ||
| Data-Race Safety for the Masses | Holly Borla | 24m |
Swift 6 adds static data-race safety to its actor model by implementing a region-based type system adapted from the PLDI’22 Fearless Concurrency paper… | ||
| The First Six Years in the Development of Polonius, an Improved Borrow Checker | Amanda Stjerna | 32m |
Polonius is an overhaul of Rust’s borrow checker that replaces lifetime points-in-CFG with lifetimes as sets of loans, adds per-program-point dynamic outlives… | ||
| Ordered Types for Typestate | Peter Thiemann | 31m |
Derives a calculus that encodes typestate as sets of allowed future traces and uses ordered context semicolons as temporal consumption order, so borrows are… | ||
| Visualizing and Explaining Rust's Ownership Model | Will Crichton | 56m |
Provides a concrete claim: embedding an auto-generated permissions model visualization (driven from the compiler MIR and a hooked MIR interpreter) into a Rust… | ||
| Substructural Information Flow via Polymorphism | Hemant Gouni, Jonathan Aldrich | 32m |
Argues that information flow is expressible with parametric polymorphism replaces lattices, presents a prototype type system implemented in OKL/OCaml tooling… | ||
| Modular Borrowing Without Ownership or Linear Types | Lionel Parreaux | 30m |
Claims a practical way to get Rust-like temporary borrowing without ownership or linear types by tracking uses as effects and encoding forbidden regions with… | ||
| Capabilities, Effects, Ownership, and Behaviors | Colin Gordon | 25m |
Argues that capability systems must track ordering by relating a flow-sensitive static capability system to a sequential effect system whose effects are… | ||
| Offer-safe Trade of Mutable Objects | Mark Miller | 01h 39m |
Claims a practical solution: Agoric’s Zoe plus an object-capability ledger enforce offer-safety by escrowing purses and issuers so contracts never touch… | ||
| nothing matches | ||