Cover Image

Modular Verification of Differential Privacy in Probabilistic Higher-Order Separation Logic (Extended Version)

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Haselwarter, Philipp G., Aguirre, Alejandro, Gregersen, Simon Oddershede, Li, Kwing Hei, Tassarotti, Joseph, Birkedal, Lars
Format:	Preprint
Published:	2026
Subjects:	Programming Languages Logic in Computer Science
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Modular Reasoning about Error Bounds for Concurrent Probabilistic Programs (Extended Version)
by: Li, Kwing Hei, et al.
Published: (2025)

Approximate Relational Reasoning for Higher-Order Probabilistic Programs
by: Haselwarter, Philipp G., et al.
Published: (2024)

Tachis: Higher-Order Separation Logic with Credits for Expected Costs
by: Haselwarter, Philipp G., et al.
Published: (2024)

Contextual Refinement of Higher-Order Concurrent Probabilistic Programs (Extended Version)
by: Li, Kwing Hei, et al.
Published: (2025)

Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs
by: Aguirre, Alejandro, et al.
Published: (2024)

Almost-Sure Termination by Guarded Refinement
by: Gregersen, Simon Oddershede, et al.
Published: (2024)

Verifying Exact Samplers for Continuous Distributions with a Discrete Program Logic
by: de Medeiros, Markus, et al.
Published: (2026)

Logical Relations for Formally Verified Authenticated Data Structures
by: Gregersen, Simon Oddershede, et al.
Published: (2025)

Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
by: Timany, Amin, et al.
Published: (2021)

Probabilistic Concurrent Reasoning in Outcome Logic: Independence, Conditioning, and Invariants
by: Zilberstein, Noam, et al.
Published: (2024)

Tableaux for Automated Reasoning in Dependently-Typed Higher-Order Logic (Extended Version)
by: Niederhauser, Johannes, et al.
Published: (2024)

Reasoning about Weak Isolation Levels in Separation Logic
by: Mathiasen, Anders Alnor, et al.
Published: (2025)

Modelling Recursion and Probabilistic Choice in Guarded Type Theory
by: Stassen, Philipp Jan Andries, et al.
Published: (2024)

A Demonic Outcome Logic for Randomized Nondeterminism
by: Zilberstein, Noam, et al.
Published: (2024)

On Higher-Order Probabilistic Verification via the Weighted Relational Model of Linear Logic
by: Lago, Ugo Dal, et al.
Published: (2026)

Probabilistic Linear Logic Programming with an Application to Bayesian Network Computations (Extended Version)
by: Acclavio, Matteo, et al.
Published: (2026)

A General Automata Model for First-Order Temporal Logics (Extended Version)
by: Geatti, Luca, et al.
Published: (2024)

Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System
by: Kura, Satoshi, et al.
Published: (2024)

Verifying Graph Algorithms in Separation Logic: A Case for an Algebraic Approach (Extended Version)
by: Grandury, Marcos, et al.
Published: (2025)

Induction and Recursion Principles in a Higher-Order Quantitative Logic for Probability
by: Bacci, Giorgio, et al.
Published: (2025)

Practical Deductive Verification of OCaml Programs (Extended Version)
by: Pereira, Mário
Published: (2024)

Probabilistic Verification for Modular Network-on-Chip Systems (extended version)
by: Waddoups, Nick, et al.
Published: (2025)

Ordered Adjoint Logic (Extended Version)
by: Roshal, Sophia, et al.
Published: (2026)

Sharing and Linear Logic with Restricted Access (Extended Version)
by: Barenbaum, Pablo, et al.
Published: (2025)

Kuroda's Translation for Higher-Order Logic
by: Traversié, Thomas
Published: (2024)

Model Checking as Program Verification by Abstract Interpretation (Extended Version)
by: Baldan, Paolo, et al.
Published: (2025)

Efficient Probabilistic Model Checking for Relational Reachability (Extended Version)
by: Gerlach, Lina, et al.
Published: (2025)

A Nominal Approach to Probabilistic Separation Logic
by: Li, John M., et al.
Published: (2024)

Partially Finite Model Reasoning in Description Logics Extended Version
by: Gogacz, Tomasz, et al.
Published: (2026)

First-Order LTLf Synthesis with Lookback (Extended Version)
by: Winkler, Sarah
Published: (2025)

Syntactic Effectful Realizability in Higher-Order Logic
by: Cohen, Liron, et al.
Published: (2025)

Static and Dynamic Verification of OCaml Programs: The Gospel Ecosystem (Extended Version)
by: Soares, Tiago Lopes, et al.
Published: (2024)

Products of Recursive Programs for Hypersafety Verification (Extended Version)
by: Cheng, Ruotong, et al.
Published: (2025)

Unification of Deterministic Higher-Order Patterns (Full Version)
by: Niederhauser, Johannes, et al.
Published: (2026)

Higher Order Automatic Differentiation of Higher Order Functions
by: Huot, Mathieu, et al.
Published: (2021)

Mechanized Undecidability of Higher-order beta-Matching (Extended Version)
by: Dudenhefner, Andrej
Published: (2026)

Paraconsistent Semantics for Extended Fuzzy Logic Programs via Approximation Fixpoint Theory [Extended Version]
by: Kettmann, Pascal, et al.
Published: (2026)

Justification Logic for Intuitionistic Modal Logic (Extended Technical Report)
by: Marin, Sonia, et al.
Published: (2025)

Compositional Verification in Concurrent Separation Logic with Permissions Regions
by: Le, Quang Loc
Published: (2025)

Extending Action Logic with Omega Iteration
by: Pshenitsyn, Tikhon
Published: (2025)