• プログラミング言語および計算モデルに関する世界最先端の研究を行っている。特に、二つのプログラムの動作が等しいという「プログラム等価性」の一般的証明手法や、近年再注目されている「関数型プログラミング」、「軽量形式手法」とも呼ばれる「型システム」等に関する研究・普及活動を行い、大手電機メーカー技術者らとの訳書「型システム入門」は理論的専門書としては異例の大手インターネット書店プログラミング入門書2 位となった。

ソフトウェア、特にDSL（ドメイン特化言語）を含むプログラミング言語およびツールの設計・開発。関数型プログラミング、型システムないし形式手法の導入・利用。

• プログラミング言語
• 関数型言語
• 並行プロセス計算