Divergences on monads for relational program logics
From MaRDI portal
Publication:6149935
DOI10.1017/s0960129523000245arXiv2206.05716OpenAlexW4385399815MaRDI QIDQ6149935
Tetsuya Sato, Shin-ya Katsumata
Publication date: 5 March 2024
Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2206.05716
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Identifying all preorders on the subdistribution monad
- Relation lifting, a survey
- Elements of generalized ultrametric domain theory
- Notions of computation and monads
- Borel structures for function spaces
- Semantics with applications: an appetizer.
- Categorical logic and type theory
- Approximate relational Hoare logic for continuous random samplings
- Graded Hoare logic and its categorical semantics
- Graded monads and rings of polynomials
- The formal theory of monads
- Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy
- Linear dependent types for differential privacy
- Probabilistic relational reasoning for differential privacy
- Concentrated Differential Privacy: Simplifications, Extensions, and Lower Bounds
- The Algorithmic Foundations of Differential Privacy
- Simple relational correctness proofs for static analyses and program transformations
- On Divergences and Informations in Statistics and Information Theory
- Codensity Lifting of Monads and its Dual
- Extending set functors to generalised metric spaces
- Quantitative Algebraic Reasoning
- Proving Differential Privacy via Probabilistic Couplings
- Preorders on Monads and Coalgebraic Simulations
- Up-To Techniques for Behavioural Metrics via Fibrations
- A Convenient Category for Higher-Order Probability Theory
- Quantitative Behavioural Reasoning for Higher-order Effectful Programs
- Fibrational bisimulations and quantitative reasoning: Extended version
- Distance makes the types grow stronger
- Monads need not be endofunctors
- Composable and versatile privacy via truncated CDP
- A Statistical Framework for Differential Privacy
- Beyond Differential Privacy: Composition Theorems and Relational Logic for f-divergences between Probabilistic Programs
- Coupling proofs are probabilistic product programs
- Parametric effect monads and semantics of effect systems
- Markov Processes and the H-Theorem
- Theory of Cryptography
- Constraint-based synthesis of coupling proofs
This page was built for publication: Divergences on monads for relational program logics
