From the 2 of 7 linked papers with an AI index.
7 papers
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…
Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version)
Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen +3
We present Coneris, the first higher-order concurrent separation logic for reasoning about error probability bounds of higher-order concurrent probabilistic programs with higher-or…
Logical Relations for Formally Verified Authenticated Data Structures
Simon Oddershede Gregersen, Chaitanya Agarwal, Joseph Tassarotti
Authenticated data structures allow untrusted third parties to carry out operations which produce proofs that can be used to verify an operation's output. Such data structures are…
Approximate Relational Reasoning for Higher-Order Probabilistic Programs
Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre +3
Properties such as provable security and correctness for randomized programs are naturally expressed relationally as approximate equivalences. As a result, a number of relational p…