現代では、パソコンや携帯電話は言うに及ばず、交通機関や電子政府、金融取引や医療機器など、社会の根幹や人命を左右するシステムがコンピュータにより制御されている。しかし、それらのコンピュータを実際に制御しているソフトウェアは、論理的・数理的な基礎の薄弱なまま、しばしば人的努力のみによって開発されており、そのことが現実にさまざまな問題を引き起こす主因となっている。

本研究室では、このような問題に対処すべく、論理的・数理的基礎に基づいたソフトウェア開発のためのプログラミング言語・手法、ツール、計算モデル等に関する研究を行っている。以下は最近の研究テーマの例である。

プログラム等価性証明手法

二つのプログラムの振る舞いが等価であるか否かは、プログラムの最適化や検証にも密接に関連する、基本的かつ重要な問題である。我々は「環境双模倣」に基づくプログラム等価性証明手法を考案し、幅広いプログラミング言語および計算モデルに適用した。

関数プログラミング

簡単・安全かつ強力なプログラミング手法・言語として近年になり再注目されている関数プログラミングおよび関数型言語に関し、トップレベルのプログラマ・技術者・研究者らと共に世界的に著名なプログラミングコンテストの主催を担当するなど、幅広い社会的活動を行っている。

双方向変換

ソフトウェア開発においては、変換とその「逆変換」の実装がしばしば要求される。我々は「ちゃんと動く」双方向変換記述のためのプログラミング言語・手法を開発している。