Preorders on Monads and Coalgebraic Simulations. - Shin-ya Katsumata; Tetsuya Sato 001 (FoSSaCS, 2013)

Identifying All Preorders on the Subdistribution Monad. - Tetsuya Sato 001 (MFPS, 2014)

Codensity Liftings of Monads. - Shin-ya Katsumata; Tetsuya Sato 001 (CALCO, 2015)

Approximate Relational Hoare Logic for Continuous Random Samplings. - Tetsuya Sato 001 (MFPS, 2016)

*-Liftings for Differential Privacy. - Gilles Barthe; Thomas Espitau; Justin Hsu; Tetsuya Sato 001; Pierre-Yves Strub (ICALP, 2017)

Reasoning about Divergences for Relaxations of Differential Privacy. - Tetsuya Sato 001; Gilles Barthe; Marco Gaboardi; Justin Hsu; Shin-ya Katsumata (CoRR, 2017)

Formal verification of higher-order probabilistic programs. - Tetsuya Sato 001; Alejandro Aguirre 001; Gilles Barthe; Marco Gaboardi; Deepak Garg 001; Justin Hsu (CoRR, 2018)

Codensity Lifting of Monads and its Dual. - Shin-ya Katsumata; Tetsuya Sato 001; Tarmo Uustalu (Log. Methods Comput. Sci., 2018)

Approximate Span Liftings: Compositional Semantics for Relaxations of Differential Privacy. - Tetsuya Sato 001; Gilles Barthe; Marco Gaboardi; Justin Hsu; Shin-ya Katsumata (LICS, 2019)

Relational ⋆⋆ star-Liftings for Differential Privacy. - Gilles Barthe; Thomas Espitau; Justin Hsu; Tetsuya Sato 001; Pierre-Yves Strub (Log. Methods Comput. Sci., 2019)

Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, Bayesian inference, and optimization. - Tetsuya Sato 001; Alejandro Aguirre 001; Gilles Barthe; Marco Gaboardi; Deepak Garg 001; Justin Hsu (Proc. ACM Program. Lang., 2019)

Hypothesis Testing Interpretations and Renyi Differential Privacy. - Borja Balle; Gilles Barthe; Marco Gaboardi; Justin Hsu; Tetsuya Sato 001 (AISTATS, 2020)

Graded Hoare Logic and its Categorical Semantics. - Marco Gaboardi; Shin-ya Katsumata; Dominic Orchard; Tetsuya Sato 001 (ESOP, 2021)

Formalizing Statistical Beliefs in Hypothesis Testing Using Program Logic. - Yusuke Kawamoto 001; Tetsuya Sato 001; Kohei Suenaga (KR, 2021)

Higher-order probabilistic adversarial computations: categorical semantics and program logics. - Alejandro Aguirre 001; Gilles Barthe; Marco Gaboardi; Deepak Garg 001; Shin-ya Katsumata; Tetsuya Sato 001 (Proc. ACM Program. Lang., 2021)

Quasi-Borel Spaces. - Michikazu Hirata; Yasuhiko Minamide; Tetsuya Sato 001 (Arch. Formal Proofs, 2022)

Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL. - Michikazu Hirata; Yasuhiko Minamide; Tetsuya Sato 001 (ITP, 2023)

Formalizing Statistical Causality via Modal Logic. - Yusuke Kawamoto 001; Tetsuya Sato 001; Kohei Suenaga (JELIA, 2023)

Divergences on monads for relational program logics. - Tetsuya Sato 001; Shin-ya Katsumata (Math. Struct. Comput. Sci., 2023)

Program logic for higher-order probabilistic programs in Isabelle/HOL. - Michikazu Hirata; Yasuhiko Minamide; Tetsuya Sato 001 (Sci. Comput. Program., 2023)

Sound and relatively complete belief Hoare logic for statistical hypothesis testing programs. - Yusuke Kawamoto 001; Tetsuya Sato 001; Kohei Suenaga (Artif. Intell., 2024)

Formalization of Differential Privacy in Isabelle/HOL. - Tetsuya Sato 001; Yasuhiko Minamide (CPP, 2025)

Differential Privacy. - Tetsuya Sato 001; Yasuhiko Minamide (Arch. Formal Proofs, 2025)