concurrency 1concurrent separation logic 1distributed execution 1effect handlers 1formal verification 1Iris 1linearizability 1logical atomicity 1program logics 1relational reasoning 1
From the 2 of 2 linked papers with an AI index.
2 papers
cs.LO2026
Building Extensible Program Logics through Effect Handlers
Zichen Zhang, Simon Oddershede Gregersen, Joseph Tassarotti
The paper presents a method for constructing extensible program logics using effect handlers, enabling modular reasoning about effects such as concurrency, distributed execution, a…
cs.LO2026
Completeness of Logical Atomicity for Linearizability in Concurrent Separation Logic
Zichen Zhang, Simon Oddershede Gregersen, Joseph Tassarotti
The paper proves that any linearizable concurrent data structure can be given a logically atomic specification in the Iris separation logic, and demonstrates this by mechanizing pr…