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)

Standard Borel Spaces. - Michikazu Hirata (Arch. Formal Proofs, 2023)

Disintegration Theorem. - Michikazu Hirata (Arch. Formal Proofs, 2023)

S-Finite Measure Monad on Quasi-Borel Spaces. - Michikazu Hirata; Yasuhiko Minamide (Arch. Formal Proofs, 2023)

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

A Formalization of the Lévy-Prokhorov Metric in Isabelle/HOL. - Michikazu Hirata (ITP, 2024)

The Lévy-Prokhorov Metric. - Michikazu Hirata (Arch. Formal Proofs, 2024)

The Riesz Representation Theorem. - Michikazu Hirata (Arch. Formal Proofs, 2024)

Coproduct Measure. - Michikazu Hirata (Arch. Formal Proofs, 2024)

Differential Privacy using Quasi-Borel Spaces. - Michikazu Hirata (Arch. Formal Proofs, 2025)