Search

• < Previous
• 1
• Next >

---

Semantics of Separation-Logic Typing and Higher-order Frame Rules for Algol-like Languages

Lars Birkedal ; Noah Torp-Smith ; Hongseok Yang.

We show how to give a coherent semantics to programs that are well-specified in a version of separation logic for a language with higher types: idealized algol extended with heaps (but with immutable stack variables). In particular, we provide simple sound rules for deriving higher-order frame&nbsp;[&hellip;]

---

Relational Parametricity and Separation Logic

Lars Birkedal ; Hongseok Yang.

Separation logic is a recent extension of Hoare logic for reasoning about programs with references to shared mutable data structures. In this paper, we provide a new interpretation of the logic for a programming language with higher types. Our interpretation is based on Reynolds's relational&nbsp;[&hellip;]

---

Linearizability with Ownership Transfer

Alexey Gotsman ; Hongseok Yang.

Linearizability is a commonly accepted notion of correctness for libraries of concurrent algorithms. Unfortunately, it assumes a complete isolation between a library and its client, with interactions limited to passing values of a given data type. This is inappropriate for common programming&nbsp;[&hellip;]

---

Nested Hoare Triples and Frame Rules for Higher-order Store

Jan Schwinghammer ; Lars Birkedal ; Bernhard Reus ; Hongseok Yang.

Separation logic is a Hoare-style logic for reasoning about programs with heap-allocated mutable data structures. As a step toward extending separation logic to high-level languages with ML-style general (higher-order) storage, we investigate the compatibility of nested Hoare triples with several&nbsp;[&hellip;]

---

Two for the Price of One: Lifting Separation Logic Assertions

Jacob Thamsborg ; Lars Birkedal ; Hongseok Yang.

Recently, data abstraction has been studied in the context of separation logic, with noticeable practical successes: the developed logics have enabled clean proofs of tricky challenging programs, such as subject-observer patterns, and they have become the basis of efficient verification tools for&nbsp;[&hellip;]

---