I am an Associate Professor at the Department of Communications and Computer Engineering, Graduate School of Informatics, Kyoto University and the Department of Computer Science, School of Engineering, Kyoto University.

I study formal verification of software. Using type theory, program logic, automata theory, and other approaches, I have worked on concurrent programs, hybrid systems, smart contracts, machine learning models, computation without decrypting data (such as homomorphic encryption), and programs that perform statistical hypothesis testing. My current goal is to develop techniques that guarantee correctness without relying on human effort, in an era where AI is building software. At Kyoto University, I teach courses such as "Implementation of Programming Languages" and make my teaching materials publicly available. I welcome cross-disciplinary collaboration.