Memory Safety: Uniqueness as Separation
Authors:
- Linares ArévaloLALinares Arévalo
- Pilar SelenePSPilar Selene
- Arthur Azevedo de AmorimAAArthur Azevedo de Amorim
- Vincent JacksonVJVincent Jackson
- Liam O’ConnorLOLiam O’Connor
- Peter SchachtePSPeter Schachte
- Christine RizkallahCRChristine Rizkallah
- 31 October 2025
- book chapter
- Published by Springer Nature
- p. 3-21
Abstract
No abstract availableKeywords
This publication has 14 references indexed in Scilit:
- Cogent: uniqueness types and certifying compilationJournal of Functional Programming, 2021
- The Meaning of Memory Safety2018
- Refinement through restraint: bringing down the cost of verification2016
- Resources, concurrency, and local reasoningTheoretical Computer Science, 2007
- Single Assignment C: efficient support for high-level array operations in a functional settingJournal of Functional Programming, 2003
- Separation logic: a logic for shared mutable data structures2003
- Local Reasoning about Programs that Alter Data Structures2001
- The execution algorithm of mercury, an efficient purely declarative logic programming languageThe Journal of Logic Programming, 1996
- Guaranteeing safe destructive updates through a type system with uniqueness information for graphs1994
- Conventional and uniqueness typing in graph rewrite systems1993