113 citations · 491 across the 32 of their papers we have counts for
5 papers · 1 filter
Algebraic Laws for Weak Consistency (Extended Version)
Andrea Cerone, Alexey Gotsman, Hongseok Yang
Modern distributed systems often rely on so called weakly-consistent databases, which achieve scalability by sacrificing the consistency guarantee of distributed transaction proces…
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…
Nested Hoare Triples and Frame Rules for Higher-order Store
Jan Schwinghammer, Lars Birkedal, Bernhard Reus +1
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 language…
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…
Semantics of Separation-Logic Typing and Higher-order Frame Rules for<br> 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…