Tetsuya SATO

I am working on programming language theory, in particular formal verification of probabilistic programs.
Keywords: probabilistic programs, relational liftings, graded monad, differential privacy, formal verification, Isabelle/HOL.

• Sound and relatively complete belief Hoare logic for statistical hypothesis testing programs. Yusuke Kawamoto, Tetsuya Sato, and Kohei Suenaga.  In Artificial Intelligence, Volume 326, January 2024, 104045. [Elsevier]

• Divergences on Monads for Relational Program Logics. Tetsuya Sato and Shin-ya Katsumata. Mathematical Structures in Computer Science(MSCS), Volume 33, Special Issue 4-5: Differences and Metrics in Programs Semantics: Advances in Quantitative Relational Reasoning. April 2023, pp. 427 - 485 [MSCS]

• Program Logic for Higher-Order Probabilistic Programs in Isabelle/HOL. Michikazu Hirata, Yasuhiko Minamide, and Tetsuya Sato. In Science of Computer Programming(SCP), Volume 230, August 2023, 102993. [Elsevier]

• Relational *-Liftings for Differential Privacy. Gilles Barthe, Thomas Espitau, Justin Hsu and Tetsuya Sato and Pierre-Yves Strub. In Logical Methods in Computer Science (LMCS), Volume 15, Issue 4, December 19, 2019. (Special Issue of ICALP 2017)  [LMCS]   

• Codensity Lifting of Monads and its Dual. Shin-ya Katsumata, Tetsuya Sato and Tarmo Uustalu.  In Logical Methods in Computer Science (LMCS), October 29, 2018, Volume 14, Issue 4. (Special Issue of CALCO 2015) [LMCS]

• The Giry monad is not strong for the canonical symmetric monoidal closed structure on Meas. Tetsuya Sato.  In Journal of Pure and Applied Algebra, Volume 222, Issue 10, Pages 2888-2896, October 2018, Elsevier. [Elsevier]

• Formalization of Differential Privacy in Isabelle/HOL, Tetsuya Sato and Yasuhiko Minamide.  In Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP ’25). [doi][Isabelle/HOL source code(Github)]

• Formalizing Statistical Causality via Modal Logic, Yusuke Kawamoto, Tetsuya Sato, and Kohei Suenaga. In  Proceedings of  18th Edition of the European Conference on Logics in Artificial Intelligence (JELIA 2023). Lecture Notes in Computer Science(LNCS), vol 14281, pp 681--696, 24 September 2023. [Springer][PDF(long version)]

• Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL, Michikazu Hirata, Yasuhiko Minamide, Tetsuya Sato, In Proceedings of 14th International Conference on Interactive Theorem Proving (ITP 2023). Volume 268, LIPIcs, pages 18:1--18:18. [Dagstuhl-LZI]

• Program Logic for Higher-Order Probabilistic Programs in Isabelle/HOL.  Michikazu Hirata, Yasuhiko Minamide, and Tetsuya Sato. In Proceedings of the 16th International Symposium on Functional and Logic Programming (FLOPS 2022), volume 13215, LNCS, pp57--74, May 3, 2022. [Springer][Isabelle/HOL source code(Github)]

• Formalizing Statistical Beliefs in Hypothesis Testing Using Program Logic. Yusuke Kawamoto, Tetsuya Sato, and Kohei Suenaga. In Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning (KR2021), Main Track, Pages. 411--421, November 2021.
  [doi][PDF(long version)]

• Higher-order probabilistic adversarial computations: categorical semantics and program logics.  Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Shin-ya Katsumata, and Tetsuya Sato. In Proceedings of the ACM on Programming Languages,  Volume 5, Issue ICFP, Article No. 93,  August 2021. [ACM] (alphabetical authorship)

• Graded Hoare Logic and its Categorical Semantics. Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard, and Tetsuya Sato.  In Proceedings of 30th European Symposium on Programming (ESOP 2021),  Lecture Notes in Computer Science (LNCS), Volume 12648,  pp. 234--263,  23 March 2021. [ArXiv][Springer] (alphabetical authorship)

• Hypothesis Testing Interpretations and Renyi Differential Privacy. Borja Balle, Gilles Barthe, Marco Gaboardi, Justin Hsu, and Tetsuya Sato. In Proceedings of the Twenty Third International Conference on Artificial Intelligence and Statistics (AISTATS 2020), PMLR 108:2496-2506, 2020. [ArXiv(long version)][PMLR] (alphabetical authorship; corresponding author)

• Approximate Span Liftings: Compositional Semantics for Relaxations of Differential Privacy. Tetsuya Sato, Gilles Barthe, Marco Gaboardi, Justin Hsu, and Shin-ya Katsumata. In Proceedings of 2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Vancouver, BC, Canada, 2019, pp. 1--14. [doi]

• Formal Verification of Higher-order Probabilistic Programs.  Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, and Justin Hsu.  In Proceedings of the ACM on Programming Languages, Volume 3 Issue POPL, January 2019, Article No.38 [ACM]

• *-Liftings for Differential Privacy. Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, and Pierre-Yves Strub.  In proceedings of ICALP 2017, Volume 80, LIPIcs, Pages 102:1--102:12, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik. [Dagstuhl-LZI] (alphabetical authorship)

• Approximate Relational Hoare Logic for Continuous Random Samplings. Tetsuya Sato.  In Proceedings of MFPS 2016, Volume 325, ENTCS, Pages 277--298, Elsevier. [Elsevier]

• Codensity Liftings of Monads. Shin-ya Katsumata and Tetsuya Sato.  In Proceedings of CALCO 2015, Volume 35, LIPIcs, pages 156--170, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik. [Dagstuhl-LZI]

• Identifying All Preorders on the Subdistribution Monad. Tetsuya Sato.  In Proceedings of MFPS 2014, Volume 308, ENTCS, pages 309--327, Elsevier. [Elsevier]

• Preorders on Monads and Coalgebraic Simulations. Shin-ya Katsumata and Tetsuya Sato.  In Proceedings of FoSSaCS 2013, Volume 7794, LNCS, pages 145--160, Springer. [Springer]

• An Investigation of Preorders on the Subdistribution Monad and their TT-Simulations. Tetsuya Sato.  In CALCO early ideas 2013 selected papers, 33--47.  [PDF(CiteSeerX)][Author's version]

• A probabilistic monad with nondeterminism for coalgebraic trace semantics. Tetsuya Sato.  In CALCO Young Researchers Workshop CALCO-jnr 2011 selected papers, pages 12--27, University of Southampton. [University of Southampton]

• Divergences on Monads and Relational Liftings. Tetsuya Sato and Shin-ya Katsumata, Short Contribution of  CMCS 2020 [Programme]

• A nondeterministic probabilistic monad for deterministic schedulers on probabilistic automata. Tetsuya Sato. Master thesis, Kyoto University. [PDF]

• Best Student Contribution Award, for the paper "Preorders on Monads and Coalgebraic Simulations" by Shin-ya Katsumata and Tetsuya Sato, 16th Europian Joint Conference on Theory and Practice of Software, ETAPS 2013, Rome, Italy (March 2013) 

• Formalization of Differential Privacy in Isabelle/HOL. The 14th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2025), Denver, CO, USA (January 21, 2025)

• Differential Privacy in Isabelle/HOL. NII Shonan Meeting NO.164: Differential Privacy and its Applications, Shonan Village Center (October 30, 2024)

• Formalization of Differential Privacy in Isabelle/HOL. 60th TRS Meeting, AIST Tokyo Waterfront Annex (October 8, 2024).

• Towards Formal Verification of Differential Privacy in Isabelle/HOL.  8th Franco-Japanese Cybersecurity Workshop, ENSC, Talence, France, (Hybrid session; November 29, 2023), Invited Talk.

• On Hypothesis Testing Interpretations of Renyi Differential Privacy.  7th Franco-Japanese Cybersecurity Workshop, Keio University, (Hybrid session; October 24, 2022), Invited Talk.

• Graded Hoare Logic and its Categorical Semantics. 30th European Symposium on Programming (ESOP 2021), Online, (Live session; March 31, 2021)

• Divergences on Monads and Relational Liftings.  15th IFIP WG 1.3 International Workshop on Coalgebraic Methods in Computer Science (CMCS 2020), Online, (Live session; October 12, 2020)[Short paper]

• Hypothesis Testing Interpretations and Renyi Differential Privacy. The 23rd International Conference on Artificial Intelligence and Statistics (AISTATS 2020), Online (Pre-recorded; August 26 - 28, 2020)

• On Formal Verification of Differential Privacy and Statistical Divergences.  ERATO MMSD Seminar Talk. Takebashi Site, ERATO Hasuo Project, Hitotsubashi, Tokyo (July 31, 2019).  

• Approximate Span Liftings: Compositional Semantics for Relaxations of Differential Privacy.  Thirty-Fourth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2019), SFU Harbour Centre, Vancouver, Canada (June 27, 2019)

• Formal Verification of Higher-order Probabilistic Programs. The 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019), Cascais, Portugal (January 16, 2019)

• Renyi Differential Privacy and Verification. Privacy Tools Retreat, Harvard Law School, Boston, Massachusetts, USA (October 30, 2018).

• Approximate Relational Hoare Logic for Continuous Random Samplings. The 32nd Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXII), Pittsburgh, Pennsylvania, USA (May 25, 2016).

• Identifying All Preorders on the Subdistribution Monad. Mathematical Foundations of Programming Semantics Thirtieth Conference (MFPS XXX), Ithaca, New York, USA (June 12, 2014)

• Simulations for Discrete Probabilistic Systems via Preorder TT-liftings. CALCO Early Ideas Workshop, Warsaw, Poland (September 2, 2013)

• Preorders on Monads and Coalgebraic Simulations. 16th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2013), Rome, Italy (March 18, 2013)

• A nondeterministic probabilistic monad with nondeterminism for coalgebraic trace semantics. CALCO Young Researchers Workshop: CALCO-jnr 2011, Winchester, Hampshire, United Kingdom (August 29, 2011)

• 差分プライバシーの検証と形式化 . Joint Seminar on Programming Languages(PL合同セミナー) 、東京科学大学大岡山キャンパス西８号館、東京都目黒区大岡山、2025年2月27日

• Isabelle/HOL を用いた 差分プライバシーの形式的検証. 日本応用数理学会2024年度年会 (招待講演)、京都大学理学部６号館、京都府京都市、2024年9月15日

• Isabelle/HOLによる差分プライバシーの形式的検証についての進捗報告. The 19th Theorem Proving and Provers meeting (TPP 2023). 東京工業大学、東京都目黒区、2023年10月31日

• 仮説検定による差分プライバシーの特徴付けとRenyi 差分プライバシー.  第5回ステアラボソフトウェア技術セミナー (招待講演)、オンライン、2022年9月15日

• 関係プログラム論理のための モナド上のダイバージェンス. 第24回プログラミングおよびプログラミング言語ワークショップ(PPL 2022)、オンライン、2022年3月7日

• Approximate Span-lifting Relaxations of Differential Privacy Based on Statistical Divergences. 小林直樹研究室セミナー、東京大学理学部７号館、東京都文京区、2019年10月15日

• Approximate Span Liftings: Compositional Semantics for Relaxations of Differential Privacy.  第36 回ソフトウェア科学会大会 (JSSST 2019) トップカンファレンス特別講演、芝浦工業大学芝浦キャンパス(東京都港区)、2019年8 月27日

• Approximate Relational Hoare Logic for Continuous Random Samplings. 第19 回プログラミングおよびプログラミング言語ワークショップ (PPL 2017)、山梨県笛吹市、2017年3 月9日

• Identifying All Preorders on the Subdistribution Monad. 第17 回プログラミングおよびプログラミング言語ワークショップ (PPL 2015)、愛媛県松山市、2015 年3 月4 日

• Hypothesis Testing Interpretations and Renyi Differential privacy. Theory and Practice of Differential Privacy (TPDP 2019), London, United Kingdom (November 11, 2019) [PDF]

• Reasoning about Differential Privacy and its Relaxations. Theory and Practice of Differential Privacy (TPDP 2018), Toronto, Canada (October 15 , 2018) [PDF]

• Reasoning about Differential Privacy and its Relaxations. Great Lakes Security Day 2018, Rochester, New York United States (September 14, 2018) 

• Reasoning about Divergences via Span-liftings. Probabilistic Programming Languages, Semantics, and Systems (PPS 2018), Los Angeles, California, United States (January 9, 2018) [PDF]

• Poster session in JSSST 2013 (in Japanese)[PDF]

• Poster session in PPL 2011 (in Japanese)[PDF]

• April, 2020 - present, Assistant Professor at Dept. of Mathematical and Computing Science, Institute of  Science Tokyo (former: Tokyo Institute of Technology)

• April 2020 - March 2025, Visiting Assistant Professor at National Institute of Informatics

• April, 2019 - March, 2020, Assistant Professor at Dept. of Computer and Information Science, Seikei University

• September, 2017 - February, 2019, Postdoctoral Associate at CSE, University at Buffalo, SUNY.

• April, 2015 - August, 2017, Postdoc Researcher at RIMS, Kyoto University.

• April, 2011 - March, 2015, Ph.D. in RIMS, Kyoto University.

• April, 2009 - March, 2011, M.S. in RIMS, Kyoto University. 

• April, 2005 - March, 2009, B.A. in Department of Arts and Sciences, Osaka Kyoiku University.

• April, 2002 - March, 2005, Tennoji High School attached to Osaka Kyoiku University.