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

We extend the semantics and type system of a lambda calculus equipped with common constructs to be \emph{resource-aware}. That is, reduction is instrumented to keep track of the usage of resources, and the type system guarantees, besides standard soundness, that for well-typed programs there is a computation where no needed resource gets exhausted.
The resource-aware extension is parametric on an arbitrary \emph{grade algebra}, and does not require ad-hoc changes to the underlying language. To this end, the semantics needs to be formalized in big-step style; as a consequence, expressing and proving (resource-aware) soundness is challenging, and is achieved by applying recent techniques based on coinductive reasoning.

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