ICFP/SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
Tue 14 Oct 2025 13:40 - 14:15 at Peony NE - Type systems 1 Chair(s): Hemant Gouni

Rust’s version of an ownership type system (the “borrow checker”) is hard for programmers to understand; the semantics are difficult for theorists to model; and in spite of this complexity and difficulty, many important data structures, including B-trees, polygon meshes, winged-edges, and even the relatively humble doubly-linked list, cannot be implemented straightforwardly in memory-safe Rust.

In this talk I’ll try to show how Rust-style Ownership Types can be modelled on top of the foundation of classical Object-Oriented Ownership Types.  Focusing on Ownership, rather than Borrowing, means we can think about the forest, not the individual trees — even if the trees end up walking around the forest from time to time.  I hope Treating Rust Ownership as Ownership Types offers a simpler conceptual model for novices; a more straightforward forjmal treatment for theorists;  a wider selection of safe linked structures for programmers; and perhaps even a foundation for the next generation of imperative programming language designs.

I’ll no doubt end up ranting about how building a Dafny program embodying Ownership has helped and hindered this effort. (work with Tobias Wrigstad, Sophia Drossopoulou, Suan Eisenbach, Michael Homer, Andrew Fawcett, etc)

James Noble (kjx@acm.org) is an independent creative researcher & programmer based in Wellington, New Zealand. After completing honours and doctoral degrees at Victoria University of Wellington (VUW), James worked at the University of Technology, Sydney, the Microsoft Research Institute at Macquarie University, and is recovering from a long stint as professor of computer science & software engineering at VUW.

James’s research centres around software design. This includes the design of the users’ interface, the parts of software that users have to deal with every day, and the programmers’ interface, the internal structures and organisations of software that programmers see only when they are designing, building, or modifying software.

James’s research in both of these areas is coloured by a longstanding interest in object-oriented approaches to design, and topics he has studied range from aliasing and object ownership, programming languages, design patterns, agile methodology, via usability, visualisation and computer music, to postmodernism and the semiotics of programming.

Tue 14 Oct

Displayed time zone: Perth change

13:40 - 15:20
Type systems 1IWACO at Peony NE
Chair(s): Hemant Gouni Carnegie Mellon University
13:40
35m
Keynote
Against Borrowing: Own the forest, not the trees!
IWACO
James Noble Independent. Wellington, NZ
14:15
25m
Talk
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
25m
Talk
Temporal Resource Typing: Enriching Substructural Typing for Liveness Reasoning
IWACO
Yiyuan Cao Peking University, Taro Sekiyama National Institute of Informatics
15:05
25m
Talk
Bringing Fearless Concurrency to Swift
IWACO
Mae Milano Princeton University