下の文章は不完全かつ古いです. 最新の情報については研究室紹介を見て下さいね.

「システムの数学」に向けて

計算機システム (複数の計算機からなる情報処理システム) の重要性は増すばかりですが,正しく動作せず甚大な被害をもたらす事例は枚挙に暇がありません.(たとえばAriane 5ロケットが打ち上げ失敗したりしていますね)

従って,システムの正しさを数学的に証明する形式検証 formal verification が計算機科学の大きな一分野として立ち現れてきました.私の研究はこの分野に属しますが,その中で数学的「極北」にあって,より一般的・抽象的な理論を作ろうとがんばっています.具体的には,

圏論的代数・余代数の理論
Categorical Universal Algebra & Coalgebra

という数学的道具を使って,

をやっています.