Michikazu HIRATA

I am currently working as an engineer at Nissan Motor.

I did PhD at Department of Mathematical and Computing Science, Institute of Science Tokyo (Formerly, Tokyo Institute of Technology), Japan.

My superviser was Prof. Yasuhiko Minamide.

Research Interest

Theoretical computer science, formal verification.

Formal verification with Isabelle/HOL, probabilitisc programs, formalization of mathematics.

Program Logic for Higher-Order Probabilistic Programs in Isabelle/HOL, Michikazu Hirata, Yasuhiko Minamide, Tetsuya Sato, Science of Computer Programming, Volume 230, journal version of FLOPS2022. DOI , source code

A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL, Michikazu Hirata, In: Proceedings of the 15th Conference on Interactive Theorem Proving (ITP2024), Tbilisi, Georgia. DOI, slide, source code(AFP)
Semantic Foundations of Higher-Order Probabilistic Programs in Isabelle/HOL, Michikazu Hirata, Yasuhiko Minamide, Tetsuya Sato, In: Proceedings of the 14th Conference on Interactive Theorem Proving (ITP2023), Białystok, Poland. DOI, slide, source code(AFP)
Program Logic for Higher-Order Probabilistic Programs in Isabelle/HOL, Michikazu Hirata, Yasuhiko Minamide, Tetsuya Sato, In: Proceedings of the 16th International Symposium on Functional and Logic Programming (FLOPS 2022), Online. DOI , slide, source code

A Formalization of Prokhorov's Theorem in Isabelle/HOL, TPP2024, November 25-26, 2024, Fukuoka, Japan. slide
A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL, 60th TRS Meeting, October 7-9, 2024, Tokyo, Japan.
Isabelle/HOLによるLevy-Prokhorov距離の形式化, 第26回プログラミングおよびプログラミング言語ワークショップ (PPL2024), March 5-7, 2024, Niigata, Japan. poster (in Japanese)
s-有限測度モナドを用いた確率的プログラミング言語のIsabelle/HOLによる形式化, 第25回プログラミングおよびプログラミング言語ワークショップ (PPL2023), March 6-8, 2023, Aichi, Japan. poster (in Japanese)
Isabelle/HOLによる確率的プログラム検証, the 18th Theorem Proving and Provers Meeting (TPP2022), September 29, 2022, Fukui, Japan.
Isabelle/HOLによる高階確率的プログラム検証(Formal Verification of Higher-Order Probabilistic Program in Isabelle/HOL), 日本ソフトウェア科学会第38回大会(The 38th JSSST Annual Conference), September 1, 2021, online. paper (in Japanese)

Diﬀerential Privacy using Quasi-Borel Spaces, Michikazu Hirata, 2025. AFP
Coproduct Measure, Michikazu Hirata, 2024. AFP
The Lévy-Prokhorov Metric, Michikazu Hirata, 2024. AFP
The Riesz Representation Theorem, Michikazu Hirata, 2024. AFP
Disintegration Theorem, Michikazu Hirata, 2023. AFP
S-Finite Measure Monad on Quasi-Borel Spaces, Michikazu Hirata and Yasuhiko Minamide, 2023. AFP
Standard Borel Spaces, Michikazu Hirata, 2023. AFP
Quasi-Borel Spaces, Michikazu Hirata, Yasuhiko Minamide, and Tetsuya Sato, 2022. AFP

April, 2022 – March, 2025, DSc in Department of Mathematical and Computing Science, School of Computing, Institute of Science Tokyo.*
April, 2020 – March, 2022, M.S. in Department of Mathematical and Computing Science, School of Computing, Tokyo Institute of Technology.
April, 2016 – March, 2020, B.S. in Department of Mathematics and Informatics, Faculty of Science, Chiba University.
April, 2013 – March, 2016, Funabashi high school.

* Tokyo Institute of Technology merged with Tokyo Medical and Dental University to form Institute of Science Tokyo (Science Tokyo).

April, 2023 - March, 2025, Research Fellowship for Young Scientists (DC2), Japan Society for the Promotion of Science.

Academic Excellence Award in Department of Mathematics and Informatics, Faculty of Science, Chiba University (2020). An award offered to 1 graduate in the Department (39 graduates in 2020).