3 papers
cs.PL2026
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…
cs.LO2025
Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)
Kwing Hei Li, Alejandro Aguirre, Joseph Tassarotti +1
We present Foxtrot, the first higher-order separation logic for proving contextual refinement of higher-order concurrent probabilistic programs with higher-order local state. From…
cs.LO2025
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…