21 citations · 63 across the 12 of their papers we have counts for
3 papers · 1 filter
Building Extensible Program Logics through Effect Handlers
Zichen Zhang, Simon Oddershede Gregersen, Joseph Tassarotti
One strategy for reasoning about programs that have certain kinds of effects is to use program logics that provide specialized rules for reasoning about these effects. However, dev…
Completeness of Logical Atomicity for Linearizability in Concurrent Separation Logic
Zichen Zhang, Simon Oddershede Gregersen, Joseph Tassarotti
Linearizability is a standard correctness condition for concurrent data structures. It guarantees that operations behave as if they took effect at some atomic instant between their…
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…