From the 2 of 9 linked papers with an AI index.
3 papers · 1 filter
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…
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…
Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic (Extended Version)
Philipp G. Haselwarter, Alejandro Aguirre, Simon Oddershede Gregersen +3
Differential privacy is the standard method for privacy-preserving data analysis. The importance of having strong guarantees on the reliability of implementations of differentially…