ソフトウェア基礎科学

情報基礎科学専攻

ソフトウェア基礎科学 A11 Foundations of Software Science

住井英二郎教授（Prof. Eijiro Sumii）
松田一孝准教授（Assoc. Prof. Kazutaka Matsuda）
西田雄気助教（Assis. Prof. Yuki Nishida）
Oleg Kiselyov 客員研究員（Visiting Scholar Oleg Kiselyov）

研究キーワードプログラミング言語理論、計算モデル、情報セキュリティ

「ちゃんと動く」ソフトウェア

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

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

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

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

関数プログラミング

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

双方向変換

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

国際関数型プログラミングコンテストの主催 (icfpc2011.blogspot.jp)
プログラム等価性証明手法の研究による受賞