SPLASH 2023
Sun 22 - Fri 27 October 2023 Cascais, Portugal
Thu 26 Oct 2023 11:00 - 11:18 at Room I - type systems 1 Chair(s): Max S. New

Verona is a concurrent object-oriented programming language that organises all the objects in a program into a forest of isolated regions. Memory is managed locally for each region, so programmers can control a program's memory use by adjusting objects' partition into regions, and by setting each region's memory management strategy. A thread can only mutate (allocate, deallocate) objects within one active region—its "window of mutability". Memory management costs are localised to the active region, ensuring overheads can be predicted and controlled. Moving the mutability window between regions is explicit, so code can be executed wherever it is required, yet programs remain in control of memory use. An ownership type system based on reference capabilities enforces region isolation, controlling aliasing within and between regions, yet supporting objects moving between regions and threads. Data accesses never need expensive atomic operations, and are always thread-safe.

Thu 26 Oct

Displayed time zone: Lisbon change

11:00 - 12:30
type systems 1OOPSLA at Room I
Chair(s): Max S. New University of Michigan
11:00
18m
Talk
Reference Capabilities for Flexible Memory Management
OOPSLA
Ellen Arvidsson Uppsala University, Elias Castegren Uppsala University, Sylvan Clebsch Microsoft Azure Research, Sophia Drossopoulou Imperial College London, James Noble Research & Programming, Matthew J. Parkinson Microsoft Azure Research, Tobias Wrigstad Uppsala University
DOI Pre-print
11:18
18m
Talk
A Grounded Conceptual Model for Ownership Types in Rust
OOPSLA
Will Crichton Brown University, Gavin Gray ETH Zurich, Shriram Krishnamurthi Brown University
DOI Pre-print
11:36
18m
Talk
Inference of Resource Management Specifications
OOPSLA
Narges Shadab University of California at Riverside, Pritam Gharat Microsoft Research, Shrey Tiwari Microsoft Research, Michael D. Ernst University of Washington, Martin Kellogg New Jersey Institute of Technology, Shuvendu K. Lahiri Microsoft Research, Akash Lal Microsoft Research, Manu Sridharan University of California at Riverside
DOI
11:54
18m
Talk
Resource-Aware Soundness for Big-Step Semantics
OOPSLA
Riccardo Bianchini University of Genoa, Francesco Dagnino University of Genoa, Paola Giannini University of Eastern Piedmont, Elena Zucca University of Genoa
DOI
12:12
18m
Talk
Verus: Verifying Rust Programs using Linear Ghost Types
OOPSLA
Andrea Lattuada VMware Research, Travis Hance Carnegie Mellon University, Chanhee Cho Carnegie Mellon University, Matthias Brun ETH Zurich, Isitha Subasinghe UNSW Sydney, Yi Zhou Carnegie Mellon University, Jon Howell VMware Research, Bryan Parno Carnegie Mellon University, Chris Hawblitzel Microsoft Research
DOI