Approximate relational Hoare logic for continuous random samplings

DOI10.1016/j.entcs.2016.09.043zbMath1401.68206arXiv1603.01445OpenAlexW2294955337WikidataQ113317629 ScholiaQ113317629MaRDI QIDQ1744393

Tetsuya Sato

Publication date: 23 April 2018

Full work available at URL: https://arxiv.org/abs/1603.01445

zbMATH Keywords

denotational semanticsdifferential privacyGiry monadgraded monadrelational lifting

Mathematics Subject Classification ID

Database theory (68P15) Data encryption (aspects in computer science) (68P25) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads (18C15) Probability in computer science (algorithm analysis, random structures, phase transitions, etc.) (68Q87)

Related Items (4)

On bisimilarity in lambda calculi with continuous probabilistic choice ⋮ Unnamed Item ⋮ Divergences on monads for relational program logics ⋮ Graded Hoare logic and its categorical semantics

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Bisimulation through probabilistic testing
• Bisimulation for probabilistic transition systems: A coalgebraic approach
• Categories of Timed Stochastic Relations
• Probabilistic relational reasoning for differential privacy
• The Algorithmic Foundations of Differential Privacy
• Simple relational correctness proofs for static analyses and program transformations
• Proving Differential Privacy via Probabilistic Couplings
• Beyond Differential Privacy: Composition Theorems and Relational Logic for f-divergences between Probabilistic Programs
• Parametric effect monads and semantics of effect systems
• Theory of Cryptography

This page was built for publication: Approximate relational Hoare logic for continuous random samplings