From bab2a3d158404c991b1032fe080429c757b2fe2a Mon Sep 17 00:00:00 2001 From: Liam O'Connor Date: Wed, 23 Sep 2026 17:01:35 +1000 Subject: [PATCH] fix some refs --- trees/refs/cheung-oconnor-rizkallah-2022.tree | 2 +- trees/refs/linares-dajosr-2025.tree | 3 +-- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/trees/refs/cheung-oconnor-rizkallah-2022.tree b/trees/refs/cheung-oconnor-rizkallah-2022.tree index 22d0468..1490fa9 100644 --- a/trees/refs/cheung-oconnor-rizkallah-2022.tree +++ b/trees/refs/cheung-oconnor-rizkallah-2022.tree @@ -5,7 +5,7 @@ \author{liamoc} \author{crizkallah} \date{2022-01-11} -\meta{doi}{10.1145/3497775.350368} +\meta{doi}{10.1145/3497775.3503686} \meta{doi}{10.48550/arXiv.2102.09920} \tag{cogent} \tag{refereed} diff --git a/trees/refs/linares-dajosr-2025.tree b/trees/refs/linares-dajosr-2025.tree index 1b730ce..df06b60 100644 --- a/trees/refs/linares-dajosr-2025.tree +++ b/trees/refs/linares-dajosr-2025.tree @@ -8,9 +8,8 @@ \author{pschachte} \author{crizkallah} \date{2025-10-27} -%\meta{doi}{} +\meta{doi}{10.1007/978-981-95-3585-9_1} \tag{cogent} \tag{refereed} \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.} -\p{To appear.} -- 2.51.2