Automatically disproving fair termination of higher-order functional programs. - Keiichi Watanabe; Ryosuke Sato 001; Takeshi Tsukada; Naoki Kobayashi 001 (ICFP, 2016)

Higher-Order Program Verification via HFL Model Checking. - Naoki Kobayashi 001; Takeshi Tsukada; Keiichi Watanabe (ESOP, 2018)

Reduction from branching-time property verification of higher-order programs to HFL validity checking. - Keiichi Watanabe; Takeshi Tsukada; Hiroki Oshikawa; Naoki Kobayashi 001 (PEPM@POPL, 2019)

On Quasi Gyrolinear Maps between Möbius Gyrovector Spaces Induced from Finite Matrices. - Keiichi Watanabe (Symmetry, 2021)

Navier-Stokes Flow in the Exterior of a Moving Obstacle with a Lipschitz Boundary. - Tomoki Takahashi; Keiichi Watanabe (SIAM J. Math. Anal., 2025)