28 citations · 123 across the 13 of their papers we have counts for
13 papers
Formalization of Differential Privacy in Isabelle/HOL
Tetsuya Sato, Yasuhiko Minamide
Differential privacy is a statistical definition of privacy that has attracted the interest of both academia and industry. Its formulations are easy to understand, but the differen…
Formalizing Statistical Causality via Modal Logic
Yusuke Kawamoto, Tetsuya Sato, Kohei Suenaga
We propose a formal language for describing and explaining statistical causality. Concretely, we define Statistical Causality Language (StaCL) for expressing causal effects and spe…
Sound and Relatively Complete Belief Hoare Logic for Statistical Hypothesis Testing Programs
Yusuke Kawamoto, Tetsuya Sato, Kohei Suenaga
We propose a new approach to formally describing the requirement for statistical inference and checking whether a program uses the statistical method appropriately. Specifically, w…
Divergences on Monads for Relational Program Logics
Tetsuya Sato, Shin-ya Katsumata
Several relational program logics have been introduced for integrating reasoning about relational properties of programs and measurement of quantitative difference between computat…
Higher-order probabilistic adversarial computations: Categorical semantics and program logics
Alejandro Aguirre, Gilles Barthe, Marco Gaboardi +3
Adversarial computations are a widely studied class of computations where resource-bounded probabilistic adversaries have access to oracles, i.e., probabilistic procedures with pri…
Graded Hoare Logic and its Categorical Semantics
Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard +1
Deductive verification techniques based on program logics (i.e., the family of Floyd-Hoare logics) are a powerful approach for program reasoning. Recently, there has been a trend o…
Hypothesis Testing Interpretations and Renyi Differential Privacy
Borja Balle, Gilles Barthe, Marco Gaboardi +2
Differential privacy is a de facto standard in data privacy, with applications in the public and private sectors. A way to explain differential privacy, which is particularly appea…
Codensity Lifting of Monads and its Dual
Shin-ya Katsumata, Tetsuya Sato, Tarmo Uustalu
We introduce a method to lift monads on the base category of a fibration to its total category. This method, which we call codensity lifting, is applicable to various fibrations wh…
Formal verification of higher-order probabilistic programs
Tetsuya Sato, Alejandro Aguirre, Gilles Barthe +3
Probabilistic programming provides a convenient lingua franca for writing succinct and rigorous descriptions of probabilistic models and inference tasks. Several probabilistic prog…
Approximate Span Liftings
Tetsuya Sato, Gilles Barthe, Marco Gaboardi +2
We develop new abstractions for reasoning about relaxations of differential privacy: Rényi differential privacy, zero-concentrated differential privacy, and truncated concentrated…
Relational -Liftings for Differential Privacy
Gilles Barthe, Thomas Espitau, Justin Hsu +2
Recent developments in formal verification have identified approximate liftings (also known as approximate couplings) as a clean, compositional abstraction for proving differential…
The Giry Monad is not Strong for the Canonical Symmetric Monoidal Closed Structure on Meas
Tetsuya Sato
We show that the Giry monad is not strong with respect to the canonical symmetric monoidal closed structure on the category Meas of all measurable spaces and measurable functions.
Approximate Relational Hoare Logic for Continuous Random Samplings
Tetsuya Sato
Approximate relational Hoare logic (apRHL) is a logic for formal verification of the differential privacy of databases written in the programming language pWHILE. Strictly speaking…