my forest
add news about aplas paper
+38
-1
+5
-1
trees/news.tree
+5
-1
trees/news.tree
···
4
4
\p{See also [Weeknotes](loc-001B)}
5
5
\table{
6
6
\tr{
7
-
\th{ 21.07.20 }
7
+
\th{ 25.07.22 }
8
+
\td{ [Selene](selene)'s paper, [[linares-dajosr-2025]], has been accepted to [[aplas25]]!}
9
+
}
10
+
\tr{
11
+
\th{ 25.07.20 }
8
12
\td{[[miowu]] and [[joshbrown]] are starting their Honours projects with me this semester, working on [the next generation of the Holbert proof assistant](loc-000V). }
9
13
}
10
14
\tr{
+6
trees/people/adeamorim.tree
+6
trees/people/adeamorim.tree
+6
trees/people/pschachte.tree
+6
trees/people/pschachte.tree
+4
trees/places/rit.tree
+4
trees/places/rit.tree
+17
trees/refs/linares-dajosr-2025.tree
+17
trees/refs/linares-dajosr-2025.tree
···
1
+
\title{Memory Safety: Uniqueness as Separation}
2
+
\taxon{Reference}
3
+
\meta{venue}{[[aplas25]]}
4
+
\author{selene}
5
+
\author{vjackson}
6
+
\author{adeamorim}
7
+
\author{liamoc}
8
+
\author{pschachte}
9
+
\author{crizkallah}
10
+
\date{2025-10-27}
11
+
%\meta{doi}{}
12
+
\tag{cogent}
13
+
\tag{refereed}
14
+
\p{This paper is the fulfillment of the research I envisioned in [my paper at VIMPL of a similar name](oconnor-linares-rizkallah-2023).}
15
+
\p{Programming languages with uniqueness type systems prevent pointer aliasing, simplifying memory safety reasoning. However, code implemented in these languages often interoperates through foreign function interfaces with external components implemented in languages lacking the same level of static safety guarantees. To verify safe updates in a combined system, one must manually verify that the external components preserve the safety invariants of the uniqueness type system. In particular, recent work showed that one can manually discharge such obligations on C components from a cross-language Cogent-C system by directly reasoning about the C code in higher-order logic. However, even for simple examples, discharging the uniqueness safety obligations, known as frame conditions, within a logic not specifically designed for direct reasoning in terms of heaps and pointers was not ideal. Separation logic is an established logic that facilitates reasoning about imperative programs by localising reasoning to the parts of the heap that the program mutates. This raises a vital question. Can we use separation logic to discharge the safety obligations imposed by uniqueness types? The answer is yes. This paper demonstrates that the frame conditions can be inferred from particular separation logic triples and, hence, discharged by reasoning using separation logic. We identify and verify the soundness of specific separation logic triples that imply the frame conditions imposed by a uniqueness type system.}
16
+
17
+
\p{To appear.}