1988年東京工業大学理学部情報科学科卒業． 1990年同大学院理工学研究科情報科学専攻修士課程修了． 同年日本電信電話株式会社入社． 現在コミュニケーション科学基礎研究所主幹研究員， 協創情報研究部情報基礎理論研究グループ グループリーダ． 型理論とロジカルフレームワーク， フォーマルメソッド（数理的技法）， コンピュータセキュリティの研究に従事． 博士（工学）（東京工業大学）． 日本ソフトウェア科学会，日本応用数理学会，情報処理学会， Association for Computing Machinery (ACM) 各会員． （もう少し詳しい略歴はこちら．）
論理は数学を支える基盤と考えられています． 実際，数学では「＜Ａ＞が成り立つ．一方＜ＡならばＢ＞も成り立つ．よって＜Ｂ＞が成り立つ」といった論理的な推論規則を組み合わせて証明を構築していきます． しかし，どうして「＜Ａ＞が成り立つ．一方＜ＡならばＢ＞も成り立つ．よって＜Ｂ＞が成り立つ」と言えるのでしょう？ その推論規則がなぜ妥当なのか，根拠を問いたくなる人はいませんか？ ひょっとしたら，ある種の初等的な数学的構造（と言ってよいのかどうかわかりませんが，そのような感じの構造）が論理の下には潜んでおり，それこそが論理を支える基盤なのではないか…などと考えています．
しかし，そんな哲学的なことばかり考えていますと疲れてしまいますので，論理を応用することも考えています (こちらがメイン((苦)笑))． 論理的な手法を用い，ソフトウェアの安全性を検証する研究を進めています．